BoundaryBumping.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Boundary bumping for compact continua

This is the compact-space argument used in the small-disk and generic-level lemmas of the uniformization manuscript. It does not assume local connectedness of the continuum.

theorem OAI.CircleDomainRigidity.component_meets_frontier line 19

Source documentation

Every component of a proper closed subset of a compact connected space meets its boundary.

theorem component_meets_frontier
    {X : Type*} [TopologicalSpace X] [CompactSpace X] [T2Space X]
    [PreconnectedSpace X] {F : Set X} (hF : IsClosed F) (hproper : F ≠ univ)
    {x : X} (hx : x ∈ F) :
    (connectedComponentIn F x ∩ frontier F).Nonempty := by
…

theorem OAI.CircleDomainRigidity.continuum_subset_closed_of_totallyDisconnected line 75

Source documentation

Adjoining totally disconnected dust to a closed set creates no new nondegenerate continuum. This is the first small-disk lemma of the paper.

theorem continuum_subset_closed_of_totallyDisconnected
    {X : Type*} [TopologicalSpace X] [T2Space X]
    {C F B : Set X} (hC : IsCompact C) (hconn : IsConnected C)
    (hnt : C.Nontrivial) (hF : IsClosed F) (hB : IsTotallyDisconnected B)
    (hsub : C ⊆ F ∪ B) : C ⊆ F := by
…