Documentation

LeanPool.ClassificationOfSurfaces.Moise.PuncturedSurface

Punctured surface charts #

The disk and half-disk models used by the Moise construction remain path-connected after deleting finitely many points. The disk case transports the corresponding theorem for the Euclidean plane through Homeomorph.unitBall. For a half-disk, we delete the finite preimage under the fold from the doubled disk, connect there, and fold the resulting path back.

These local results are the input for proving that a connected surface remains connected after deleting a finite set. That theorem, in turn, rules out multiple dual components in a completed surface triangulation.

source
def LeanEval.Topology.ClassificationOfSurfaces.Moise.foldDiskToHalfDisk :
↑ChartKind.disk.modelRegion → ↑ChartKind.halfDisk.modelRegion

Fold the open unit disk onto the open half-disk.

Equations
Instances For
    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.continuous_foldDiskToHalfDisk :
    Continuous foldDiskToHalfDisk

    Folding the disk onto the half-disk is continuous.

    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.finite_preimage_foldDiskToHalfDisk (s : Set ↑ChartKind.halfDisk.modelRegion) (hs : s.Finite) :
    (foldDiskToHalfDisk ⁻¹' s).Finite

    The inverse image of a finite set under the disk fold is finite. Each fiber is contained in the two-point set consisting of a point and its reflection across the boundary line.

    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.surjective_foldDiskToHalfDisk :
    Function.Surjective foldDiskToHalfDisk

    Folding the disk onto the half-disk is surjective.

    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.diskModel_compl_finite_isPathConnected (s : Set ↑ChartKind.disk.modelRegion) (hs : s.Finite) :
    IsPathConnected sᶜ

    An open disk with finitely many points deleted is path-connected.

    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.halfDiskModel_compl_finite_isPathConnected (s : Set ↑ChartKind.halfDisk.modelRegion) (hs : s.Finite) :
    IsPathConnected sᶜ

    An open half-disk with finitely many points deleted is path-connected.

    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.isPathConnected_compl_finite (k : ChartKind) (s : Set ↑k.modelRegion) (hs : s.Finite) :
    IsPathConnected sᶜ

    Either Moise chart model remains path-connected after deleting finitely many points.

    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.isPathConnected_modelRegion_diff_finite (k : ChartKind) (s : Set Plane) (hs : s.Finite) :
    IsPathConnected (k.modelRegion \ s)

    The underlying planar model region remains path-connected after deleting a finite ambient set.

    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.isPathConnected_compl_finite_subtype {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) (s : Set ↑c.domain) (hs : s.Finite) :
    IsPathConnected sᶜ

    A Moise chart domain, as a subtype, remains path-connected after deleting finitely many points.

    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.isPathConnected_domain_diff_finite {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) (s : Set S) (hs : s.Finite) :
    IsPathConnected (c.domain \ s)

    The ambient chart domain remains path-connected after deleting a finite subset of the surface.

    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.isConnected_compl_finite_of_locally_pathConnected {S : Type u_1} [TopologicalSpace S] [T1Space S] [ConnectedSpace S] {F : Set S} (hF : F.Finite) (hlocal : ∀ p ∈ F, ∃ (U : Set S), IsOpen U ∧ p ∈ U ∧ IsPathConnected (U \ F)) :
    IsConnected Fᶜ

    A connected T1 space stays connected after deleting a finite set if every deleted point has an open neighborhood whose complement of the whole finite set is path-connected.

    For a putative separation of the complement, each deleted point is assigned to the unique side containing its punctured neighborhood. Restoring the assigned points then produces two disjoint open sets covering the original connected space.

    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.isConnected_compl_finite_surface {S : Type u_1} [TopologicalSpace S] [T1Space S] [ConnectedSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] {F : Set S} (hF : F.Finite) :
    IsConnected Fᶜ

    A connected surface charted on the Euclidean half-plane remains connected after deleting finitely many points.