GenericLevelTopology.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Topology of finite-length level unions

The compact spaces here are a quotient level union and its physical preimage, with the induced metrics. Thus finite Hausdorff length on G is finite physical level length, not finite length of a planar open domain. Compact totally disconnected quotient dust supplies the small disjoint covers and hence compact physical cores. All counting and local connectedness conclusions are then proved.

theorem OAI.CircleDomainRigidity.finite_large_continuum_bound_of_compact_quotient_dust line 24

Source documentation

Finite physical length and compact totally disconnected quotient dust imply the finite bound on disjoint large subcontinua.

theorem finite_large_continuum_bound_of_compact_quotient_dust
    {X Y : Type*} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X]
    [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y]
    (π : Y → X) (hπ : Continuous π) (hsurj : Function.Surjective π)
    (hfiber : ∀ x, IsConnected (π ⁻¹' {x})) {G : Set Y} (hG : IsOpen G)
    {B : Set X} (hB : IsCompact B) (hTD : IsTotallyDisconnected B)
    (hdust : π '' Gᶜ ⊆ B) (hlength : (μH[1] : Measure Y) G < ∞) :
    HasFiniteLargeContinuumBound X := by
…

Mentions: OAI.CircleDomainRigidity.HasFiniteLargeContinuumBound

theorem OAI.CircleDomainRigidity.generic_level_topology_of_compact_quotient_dust line 60

Source documentation

The topological consequences in generic-level-continua (ii) and the countability and local-connectedness part of (iii), from the actual finite-length and quotient-dust hypotheses.

theorem generic_level_topology_of_compact_quotient_dust
    {X Y : Type*} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X]
    [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y]
    (π : Y → X) (hπ : Continuous π) (hsurj : Function.Surjective π)
    (hfiber : ∀ x, IsConnected (π ⁻¹' {x})) {G : Set Y} (hG : IsOpen G)
    {B : Set X} (hB : IsCompact B) (hTD : IsTotallyDisconnected B)
    (hdust : π '' Gᶜ ⊆ B) (hlength : (μH[1] : Measure Y) G < ∞) :
    HasFiniteLargeContinuumBound X ∧
      {C : Set X | (∃ x, C = connectedComponent x) ∧ C.Nontrivial}.Countable ∧
      ∀ C : Set X, IsCompact C → IsConnected C → LocallyConnectedSpace C := by
…

Mentions: OAI.CircleDomainRigidity.HasFiniteLargeContinuumBound