SinglePhysicalDisk.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A single smooth physical disk about a quotient singleton

Connectedness of the fiber upgrades the finite disjoint cover to a single disk. The general open-family lemma does not need finiteness.

theorem OAI.CircleDomainRigidity.exists_member_containing_connected_set line 17
theorem OAI.CircleDomainRigidity.isConnected_finite_fiber line 42

theorem OAI.CircleDomainRigidity.SmoothPhysicalDiskCover.exists_single_disk line 61

Source documentation

A finite disjoint disk cover of a connected physical fiber contains one disk covering that entire fiber.

theorem SmoothPhysicalDiskCover.exists_single_disk
    {X : Type*} {π : Sphere → X} {x : X} {V F : Set X} {G : Set Sphere}
    (hcover : SmoothPhysicalDiskCover π x V F G)
    (hfiber : IsConnected {z : ℂ | π (z : Sphere) = x}) :
    ∃ (H : ℂ ≃ₜ ℂ) (γ : Circle → ℂ),
      {z : ℂ | π (z : Sphere) = x} ⊆ jordanInterior H ∧
      closure (jordanInterior H) ⊆ (fun z : ℂ => π (z : Sphere)) ⁻¹' V ∧
      ContMDiff (𝓡 1) (𝓘(ℝ, ℂ)) ∞ γ ∧ Topology.IsEmbedding γ ∧
      frontier (jordanInterior H) = range γ ∧
      ∀ z ∈ frontier (jordanInterior H), (z : Sphere) ∈ G ∧ π (z : Sphere) ∉ F := by
…

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

theorem OAI.CircleDomainRigidity.exists_single_small_physical_disk line 87

Source documentation

Exact single-disk form of the small physical neighborhood statement for the actual component quotient.

theorem exists_single_small_physical_disk
    (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