MooreReduction.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The published Moore input and its application

Published input: R. L. Moore, Concerning upper semi-continuous collections of continua, Trans. Amer. Math. Soc. 27 (1925), 416–428. The proposition MooreSphereDecomposition is the closed-equivalence-relation form of the sphere decomposition theorem needed in §2 of the Koebe manuscript. It is an explicit hypothesis, not a global axiom. The application below verifies its hypotheses for complementary components and proves the dust conclusion separately.

def OAI.CircleDomainRigidity.MooreSphereDecomposition line 25
Source documentation
The precise topological published input. Singleton classes are allowed; every other class is connected and has connected nonempty complement.
```
def MooreSphereDecomposition : Prop :=
…
```
def OAI.CircleDomainRigidity.componentSetoid line 34
Source documentation
The equivalence relation collapsing exactly the complementary components.
```
def componentSetoid (G : Set Sphere) : Setoid Sphere where
…
```
Mentions: OAI.CircleDomainRigidity.Sphere
theorem OAI.CircleDomainRigidity.componentSetoid_class_of_mem line 55
theorem OAI.CircleDomainRigidity.componentSetoid_class_of_notMem line 65
theorem OAI.CircleDomainRigidity.locallyConnected_sphere line 74

theorem OAI.CircleDomainRigidity.componentSphereQuotient_of_moore line 83

Source documentation

The component quotient in §2, conditional solely on the named published Moore theorem. Its total-disconnectedness conclusion is proved here.

theorem componentSphereQuotient_of_moore (hMoore : MooreSphereDecomposition)
    {G : Set Sphere} (hopen : IsOpen G) (hconn : IsConnected G) :
    ∃ π : Sphere → Sphere, Continuous π ∧ IsClosedMap π ∧ Function.Surjective π ∧
      (∀ x y, π x = π y ↔
        x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x)) ∧
      IsTotallyDisconnected (π '' G)ᶜ := by
…

Mentions: OAI.CircleDomainRigidity.MooreSphereDecomposition, OAI.CircleDomainRigidity.Sphere