ComponentLocalization.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Localizing nondegenerate components

Boundary bumping turns a nondegenerate continuum through a point into one in any prescribed neighborhood. This is the localization used in the lower-grid obstacle argument. Totally disconnected dust cannot destroy a singleton component of a compact closed obstacle.

theorem OAI.CircleDomainRigidity.exists_nontrivial_subcontinuum_in_open line 18

theorem OAI.CircleDomainRigidity.component_eq_singleton_of_local_no_continuum line 62

Source documentation

To rule out a nondegenerate component, it suffices to rule out small subcontinua through the point in one open neighborhood.

theorem component_eq_singleton_of_local_no_continuum
    {X : Type*} [TopologicalSpace X] [CompactSpace X] [T2Space X]
    {F U : Set X} (hF : IsClosed F) {x : X} (hx : x ∈ F)
    (hU : IsOpen U) (hxU : x ∈ U)
    (hno : ∀ D : Set X, IsCompact D → IsConnected D → x ∈ D →
      D ⊆ F ∩ U → ¬ D.Nontrivial) :
    connectedComponentIn F x = {x} := by
…

theorem OAI.CircleDomainRigidity.component_union_dust_eq_singleton line 85

Source documentation

Adding compact totally disconnected dust preserves every singleton component of a closed obstacle and gives singleton components off it.

theorem component_union_dust_eq_singleton
    {X : Type*} [TopologicalSpace X] [CompactSpace X] [T2Space X]
    {F B : Set X} (hF : IsClosed F) (hB : IsClosed B)
    (htd : IsTotallyDisconnected B) {x : X} (hx : x ∈ F ∪ B)
    (hsing : x ∈ F → connectedComponentIn F x = {x}) :
    connectedComponentIn (F ∪ B) x = {x} := by
…

theorem OAI.CircleDomainRigidity.component_finite_union_eq_singleton line 113

Source documentation

Near a point, a finite closed level union only uses the levels which contain that point. A singleton component in this smaller union is therefore a singleton component in the entire union.

theorem component_finite_union_eq_singleton
    {X ι : Type*} [TopologicalSpace X] [CompactSpace X] [T2Space X]
    (s : Finset ι) (H : ι → Set X) (hH : ∀ i ∈ s, IsClosed (H i))
    {x : X} (hx : x ∈ ⋃ i ∈ s, H i)
    (hpresent : connectedComponentIn (⋃ i ∈ s, ⋃ (_ : x ∈ H i), H i) x = {x}) :
    connectedComponentIn (⋃ i ∈ s, H i) x = {x} := by
…