SaturatedDisks.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Saturation of physical Jordan interiors

A connected quotient fiber cannot cross a boundary consisting of singleton fibers. Thus physical Jordan interiors whose boundaries lie in the original domain are saturated, and project to open quotient neighborhoods. This is the saturation assertion preceding the small-disks lemma in Section 1.

theorem OAI.CircleDomainRigidity.preimage_image_open_of_singleton_boundary_fibers line 19
theorem OAI.CircleDomainRigidity.closure_sphere_image_jordanInterior line 52
theorem OAI.CircleDomainRigidity.frontier_sphere_image_jordanInterior line 61

theorem OAI.CircleDomainRigidity.preimage_image_jordanInterior_of_component_collapse line 71

Source documentation

Physical Jordan disks with boundary in the domain are saturated for the actual component-collapse quotient.

theorem preimage_image_jordanInterior_of_component_collapse
    {Y : Type*} (G : Set Sphere) (π : Sphere → Y) (hsurj : Surjective π)
    (hr : ∀ x y, π x = π y ↔
      x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x))
    (H : ℂ ≃ₜ ℂ) (hboundary : ∀ z ∈ frontier (jordanInterior H), (z : Sphere) ∈ G) :
    π ⁻¹' (π '' (((↑) : ℂ → Sphere) '' jordanInterior H)) =
      ((↑) : ℂ → Sphere) '' jordanInterior H := by
…

Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.jordanInterior

theorem OAI.CircleDomainRigidity.isOpen_image_jordanInterior_of_component_collapse line 89

Source documentation

The saturated physical disk projects to an open quotient neighborhood.

theorem isOpen_image_jordanInterior_of_component_collapse
    {Y : Type*} [TopologicalSpace Y]
    (G : Set Sphere) (π : Sphere → Y) (hπ : Continuous π)
    (hclosed : IsClosedMap π) (hsurj : Surjective π)
    (hr : ∀ x y, π x = π y ↔
      x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x))
    (H : ℂ ≃ₜ ℂ) (hboundary : ∀ z ∈ frontier (jordanInterior H), (z : Sphere) ∈ G) :
    IsOpen (π '' (((↑) : ℂ → Sphere) '' jordanInterior H)) := by
…

Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.jordanInterior