ComponentTopology.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Topological parts of the component argument

The quotient theorem below proves the totally disconnected dust conclusion from the component-collapse properties of the quotient. Moore's 1925 sphere-decomposition theorem supplies the sphere realization; that published input is not assumed to provide the dust conclusion for free.

theorem OAI.CircleDomainRigidity.IsComplementaryComponent.disjoint_of_ne line 20
theorem OAI.CircleDomainRigidity.countable_complementaryComponents_with_interior line 31
Source documentation
No countability is imposed on point components. The components with nonempty interior are countable by separability.
```
theorem countable_complementaryComponents_with_interior (G : Set Sphere) :
    {K : Set Sphere | IsComplementaryComponent G K ∧ (interior K).Nonempty}.Countable := by
…
```
Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.IsComplementaryComponent

theorem OAI.CircleDomainRigidity.totallyDisconnected_quotient_complement line 45

Source documentation

The component quotient of a closed complement has totally disconnected omitted set. The hypotheses precisely express the topological quotient, saturation of the domain, connected fibers, and collapse of each complementary component; they contain no uniformization or circle-domain conclusion.

theorem totallyDisconnected_quotient_complement
    {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    (G : Set X) (hG : IsOpen G) (π : X → Y) (hπ : IsQuotientMap π)
    (hsat : π ⁻¹' (π '' G) = G)
    (hfiber : ∀ y, IsConnected (π ⁻¹' {y}))
    (hcomponent : ∀ x ∈ Gᶜ, π ⁻¹' {π x} = connectedComponentIn Gᶜ x) :
    IsTotallyDisconnected (π '' G)ᶜ := by
…

theorem OAI.CircleDomainRigidity.totallyDisconnected_of_component_collapse line 77

Source documentation

A direct form for the decomposition used in both manuscripts: points of the domain remain singletons and precisely the complementary components are collapsed. Closedness and continuity are the topological quotient input.

theorem totallyDisconnected_of_component_collapse
    {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    (G : Set X) (hG : IsOpen G) (π : X → Y) (hcont : Continuous π)
    (hclosed : IsClosedMap π) (hsurj : Function.Surjective π)
    (hrel : ∀ x y, π x = π y ↔
      x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x)) :
    IsTotallyDisconnected (π '' G)ᶜ := by
…