FiniteChartConnectivity.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Passing a connected exterior through the finite sphere chart

Deleting an interior point from a connected set preserves connectedness when that point has a connected punctured neighborhood. Applied at infinity, this turns the connected sphere inverse image of a quotient exterior into the connected unbounded planar exterior needed for smooth contour filling.

theorem OAI.CircleDomainRigidity.puncture_subset_of_boundary_color line 19

theorem OAI.CircleDomainRigidity.isPreconnected_puncture_of_connected_neighborhood line 65

Source documentation

A point with a connected punctured neighborhood is not a cut point of any connected set containing that neighborhood.

theorem isPreconnected_puncture_of_connected_neighborhood
    {X : Type*} [TopologicalSpace X] [T1Space X]
    {S U : Set X} {p : X} (hp : p ∉ S)
    (hconn : IsPreconnected (insert p S)) (hU : U ∈ 𝓝 p)
    (hUS : U \ {p} ⊆ S) (hpuncture : IsPreconnected (U \ {p})) :
    IsPreconnected S := by
…

theorem OAI.CircleDomainRigidity.isConnected_complex_exterior_closedBall line 86

theorem OAI.CircleDomainRigidity.finite_part_connected_unbounded line 110

Source documentation

The finite part of a connected sphere set containing a neighborhood of infinity is preconnected and unbounded.

theorem finite_part_connected_unbounded {K : Set Sphere}
    (hK : IsPreconnected K) (hinfty : ∞ ∈ interior K) :
    IsPreconnected (((↑) : ℂ → Sphere) ⁻¹' K) ∧
      ¬ Bornology.IsBounded (((↑) : ℂ → Sphere) ⁻¹' K) := by
…

Mentions: OAI.CircleDomainRigidity.Sphere

theorem OAI.CircleDomainRigidity.physical_exterior_connected_unbounded_of_quotient line 163

Source documentation

A closed quotient with connected fibers pulls a closed connected quotient exterior back to a connected unbounded physical exterior.

theorem physical_exterior_connected_unbounded_of_quotient
    {X : Type*} [TopologicalSpace X]
    (π : Sphere → X) (hπ : Continuous π) (hclosed : IsClosedMap π)
    (hsurj : Surjective π) (hfibers : ∀ x, IsConnected (π ⁻¹' {x}))
    {V : Set X} (hV : IsOpen V) (hVconn : IsConnected Vᶜ)
    (hinfty : π ∞ ∉ closure V) :
    IsPreconnected ((fun z : ℂ => π (z : Sphere)) ⁻¹' V)ᶜ ∧
      ¬ Bornology.IsBounded ((fun z : ℂ => π (z : Sphere)) ⁻¹' V)ᶜ := by
…

Mentions: OAI.CircleDomainRigidity.Sphere

theorem OAI.CircleDomainRigidity.physical_exterior_connected_unbounded_of_component_collapse line 183

Source documentation

Specialization to a component-collapse quotient.

theorem physical_exterior_connected_unbounded_of_component_collapse
    {X : Type*} [TopologicalSpace 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))
    {V : Set X} (hV : IsOpen V) (hVconn : IsConnected Vᶜ)
    (hinfty : π ∞ ∉ closure V) :
    IsPreconnected ((fun z : ℂ => π (z : Sphere)) ⁻¹' V)ᶜ ∧
      ¬ Bornology.IsBounded ((fun z : ℂ => π (z : Sphere)) ⁻¹' V)ᶜ :=
…

Mentions: OAI.CircleDomainRigidity.Sphere