SmallQuotientDisks.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Smooth physical disks from the component quotient

These statements combine compact clopen isolation, actual contour selection, the component quotient, and the infinity-chart argument. Connectedness and unboundedness of the physical exterior are conclusions of the preceding lemmas, not additional disk-selection hypotheses.

def OAI.CircleDomainRigidity.SmoothPhysicalDiskCover line 21
Source documentation
Concrete finite smooth Jordan disks covering the physical fiber of x. The indexing set is a finite subset of the regular level's components.
```
def SmoothPhysicalDiskCover {X : Type*} (π : Sphere → X) (x : X)
    (V F : Set X) (G : Set Sphere) : Prop :=
…
```
Mentions: OAI.CircleDomainRigidity.Sphere

theorem OAI.CircleDomainRigidity.smoothPhysicalDiskCover_of_component_quotient line 39

Source documentation

The small physical disk construction for a singleton component of the actual quotient obstacle.

theorem smoothPhysicalDiskCover_of_component_quotient
    (hsard : SmoothPlanarSard) (hschoenflies : PlanarSchoenflies)
    {X : Type*} [TopologicalSpace X] [CompactSpace X] [T2Space X]
    (G : Set Sphere) (π : Sphere → X) (hπ : Continuous π)
    (hclosed : IsClosedMap π) (hsurj : Surjective π)
    (hr : ∀ x y, π x = π y ↔
      x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x))
    {F V : Set X} (hF : IsClosed F) {x : X} (hx : x ∈ F)
    (hcomponent : connectedComponentIn F x = {x})
    (hV : IsOpen V) (hxV : x ∈ V) (hVconn : IsConnected Vᶜ)
    (hinfty : π OnePoint.infty ∉ closure V)
    (hbad : ∀ p ∈ Gᶜ, π p ∈ F) :
…

Mentions: OAI.CircleDomainRigidity.SmoothPlanarSard, OAI.CircleDomainRigidity.PlanarSchoenflies, OAI.CircleDomainRigidity.Sphere

theorem OAI.CircleDomainRigidity.smoothPhysicalDiskCover_after_adjoining_dust line 61

Source documentation

Adjoining the quotient dust preserves singleton components and the resulting smooth boundaries avoid both the original obstacle and dust.

theorem smoothPhysicalDiskCover_after_adjoining_dust
    (hsard : SmoothPlanarSard) (hschoenflies : PlanarSchoenflies)
    {X : Type*} [TopologicalSpace X] [CompactSpace X] [T2Space X]
    (G : Set Sphere) (π : Sphere → X) (hπ : Continuous π)
    (hclosed : IsClosedMap π) (hsurj : Surjective π)
    (hr : ∀ x y, π x = π y ↔
      x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x))
    {F B V : Set X} (hF : IsClosed F) (hB : IsClosed B)
    (hTD : IsTotallyDisconnected B) {x : X} (hx : x ∈ F ∪ B)
    (hsing : x ∈ F → connectedComponentIn F x = {x})
    (hV : IsOpen V) (hxV : x ∈ V) (hVconn : IsConnected Vᶜ)
    (hinfty : π OnePoint.infty ∉ closure V)
…

Mentions: OAI.CircleDomainRigidity.SmoothPlanarSard, OAI.CircleDomainRigidity.PlanarSchoenflies, OAI.CircleDomainRigidity.Sphere