Documentation

LeanPool.ClassificationOfSurfaces.Moise.DualConnectivity

Dual connectivity of completed surface triangulations #

A completed finite triangulation of a connected surface has connected dual graph. The proof does not require a separate cyclic-link theorem. If the faces split into two dual components, their closed carriers can meet only at triangulation vertices. Deleting that finite vertex locus would therefore disconnect the surface, contradicting finite-puncture connectivity.

source
def LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.FaceReachable {Vertex : Type u_1} (faces : Finset (Finset Vertex)) (root : Face faces) (t : Finset Vertex) :
Prop

Membership of a raw face in the dual component generated by root.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.faceReachable_iff {Vertex : Type u_1} {faces : Finset (Finset Vertex)} (root f : Face faces) :
    FaceReachable faces root ↑f ↔ Relation.ReflTransGen (FaceAdjacent faces) root f
    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.faceReachable_root {Vertex : Type u_1} {faces : Finset (Finset Vertex)} (root : Face faces) :
    FaceReachable faces root ↑root
    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.TriangleFamily.not_faceAdjacent_of_faceReachable_of_not {Vertex : Type u_1} {faces : Finset (Finset Vertex)} (root f g : Face faces) (hf : FaceReachable faces root ↑f) (hg : ¬FaceReachable faces root ↑g) :
    ¬FaceAdjacent faces f g

    A face outside the component of root cannot share an edge with a face inside it.

    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PartialTriangulation.isDualConnected_of_support_eq_univ {S : Type u_1} [TopologicalSpace S] (T : PartialTriangulation S) [T2Space S] [ConnectedSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] (hcovers : T.support = Set.univ) :
    TriangleFamily.IsDualConnected T.faces

    A finite partial triangulation which covers a connected surface has connected dual graph.

    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.faces_isDualConnected {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) [ConnectedSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] :
    TriangleFamily.IsDualConnected T.faces

    Every finite geometric triangulation of a connected surface has connected dual graph.

    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.GeometricTriangulation.surfaceIncidence {S : Type u_1} [TopologicalSpace S] (T : GeometricTriangulation S) [ConnectedSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] :
    T.SurfaceIncidence

    A finite geometric triangulation of a connected surface carries the complete incidence certificate needed by the cell-complex bridge.