Fixed-vertex stars in a surface triangulation

A geometric triangulation of a topological surface has connected links. The proof uses a punctured surface chart inside the open barycentric star of a vertex. If the fixed-vertex star had two adjacency components, their finite closed face unions would separate that punctured chart.

theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.faces_isStrongVertexStarConnected {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] : have x := ⋯; TriangleFamily.IsStrongVertexStarConnected T.faces

Every fixed-vertex face star in a geometric triangulation of a topological surface is connected through edges containing that vertex.