FinitelySuslinian.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Finite bounds on disjoint continua imply local connectedness

This is the topological implication (ii) to (iii) in the generic-level continua lemma of 047-02, Section 1. Components of a closed ball that meet its half-radius ball have uniformly positive diameter by boundary bumping. There are only finitely many of them, so the component through the center is a neighborhood of that center.

def OAI.CircleDomainRigidity.HasFiniteLargeContinuumBound line 28
Source documentation
A uniform finite bound on the number of pairwise disjoint subcontinua having any fixed positive minimum diameter.
```
def HasFiniteLargeContinuumBound (X : Type*) [MetricSpace X] : Prop :=
…
```

theorem OAI.CircleDomainRigidity.finite_large_continuum_bound_of_measure line 36

Source documentation

Finite total length gives a uniform cardinal bound when every continuum of a fixed minimum diameter pays a positive amount of that length. The geometric lower payment remains an explicit hypothesis.

theorem finite_large_continuum_bound_of_measure {X : Type*} [MetricSpace X]
    [MeasurableSpace X] [BorelSpace X] (μ : MeasureTheory.Measure X)
    [MeasureTheory.IsFiniteMeasure μ]
    (hpayment : ∀ ε : ℝ, 0 < ε → ∃ δ : ℝ, 0 < δ ∧
      ∀ C : Set X, IsCompact C → IsConnected C → ε ≤ diam C → δ ≤ μ.real C) :
    HasFiniteLargeContinuumBound X := by
…

Mentions: OAI.CircleDomainRigidity.HasFiniteLargeContinuumBound

theorem OAI.CircleDomainRigidity.finite_large_continuum_family line 60
theorem OAI.CircleDomainRigidity.closed_componentIn line 73
theorem OAI.CircleDomainRigidity.countable_disjoint_nontrivial_subcontinua line 83
Source documentation
A disjoint family of nondegenerate subcontinua is countable: for each positive reciprocal diameter threshold only finitely many can occur.
```
theorem countable_disjoint_nontrivial_subcontinua {X : Type*} [MetricSpace X]
    (hbound : HasFiniteLargeContinuumBound X) {S : Set (Set X)}
    (hS : ∀ C ∈ S, IsCompact C ∧ IsConnected C ∧ C.Nontrivial)
    (hdisj : S.Pairwise Disjoint) : S.Countable := by
…
```
Mentions: OAI.CircleDomainRigidity.HasFiniteLargeContinuumBound
theorem OAI.CircleDomainRigidity.countable_nontrivial_connectedComponents line 99
Source documentation
The nondegenerate connected components of a compact metric space are countable under the finite-continuum bound.
```
theorem countable_nontrivial_connectedComponents {X : Type*} [MetricSpace X]
    [CompactSpace X] (hbound : HasFiniteLargeContinuumBound X) :
    {C : Set X | (∃ x, C = connectedComponent x) ∧ C.Nontrivial}.Countable := by
…
```
Mentions: OAI.CircleDomainRigidity.HasFiniteLargeContinuumBound
theorem OAI.CircleDomainRigidity.closedBall_component_mem_nhds line 112
Source documentation
The component of a closed ball through its center is a neighborhood when the ambient continuum has finite bounds on large disjoint continua.
```
theorem closedBall_component_mem_nhds {X : Type*} [MetricSpace X]
    [CompactSpace X] [PreconnectedSpace X]
    (hbound : HasFiniteLargeContinuumBound X) (x : X) {r : ℝ} (hr : 0 < r) :
    connectedComponentIn (closedBall x r) x ∈ 𝓝 x := by
…
```
Mentions: OAI.CircleDomainRigidity.HasFiniteLargeContinuumBound
theorem OAI.CircleDomainRigidity.locallyConnectedSpace_of_finite_large_continuum_bound line 170
Source documentation
A compact metric continuum with uniform finite bounds on large pairwise disjoint subcontinua is locally connected.
```
theorem locallyConnectedSpace_of_finite_large_continuum_bound
    {X : Type*} [MetricSpace X] [CompactSpace X] [PreconnectedSpace X]
    (hbound : HasFiniteLargeContinuumBound X) : LocallyConnectedSpace X := by
…
```
Mentions: OAI.CircleDomainRigidity.HasFiniteLargeContinuumBound
theorem OAI.CircleDomainRigidity.HasFiniteLargeContinuumBound.subtype line 182
Source documentation
The finite bound is inherited by metric subspaces, with the same bound on cardinalities.
```
theorem HasFiniteLargeContinuumBound.subtype {X : Type*} [MetricSpace X]
    (hbound : HasFiniteLargeContinuumBound X) (K : Set X) :
    HasFiniteLargeContinuumBound K := by
…
```
Mentions: OAI.CircleDomainRigidity.HasFiniteLargeContinuumBound
theorem OAI.CircleDomainRigidity.locallyConnected_subcontinuum_of_finite_large_continuum_bound line 209
Source documentation
In particular every compact connected subcontinuum is locally connected under the ambient finite-continuum bound.
```
theorem locallyConnected_subcontinuum_of_finite_large_continuum_bound
    {X : Type*} [MetricSpace X] (hbound : HasFiniteLargeContinuumBound X)
    {K : Set X} (hK : IsCompact K) (hconn : IsConnected K) :
    LocallyConnectedSpace K := by
…
```
Mentions: OAI.CircleDomainRigidity.HasFiniteLargeContinuumBound