GridObstacles.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Singleton components of the lower-grid obstacle

At a free point, each coordinate has a unique trace, so at most one of its finitely many distinct grid levels contains the point. Pointwise compatibility for these choices excludes a nondegenerate component of the lower-grid union. Boundary bumping removes all the other levels, and adjoining compact totally disconnected dust preserves the singleton. This is the topological reduction in Step 3 of finite transfer.

theorem OAI.CircleDomainRigidity.component_finite_grid_eq_singleton line 22

Source documentation

Pointwise compatibility for every selection of one level per active label controls the entire finite grid near a point with unique traces.

theorem component_finite_grid_eq_singleton
    {X I J : Type*} [TopologicalSpace X] [CompactSpace X] [T2Space X]
    [Fintype I] [Fintype J] [Nonempty J]
    (H : I → J → Set X) (hH : ∀ i j, IsClosed (H i j)) {x : X}
    (hx : x ∈ ⋃ i, ⋃ j, H i j)
    (hunique : ∀ i j k, x ∈ H i j → x ∈ H i k → j = k)
    (hcompat : ∀ (A : Finset I) (k : I → J),
      ¬ (connectedComponentIn (⋃ i ∈ A, H i (k i)) x).Nontrivial) :
    connectedComponentIn (⋃ i, ⋃ j, H i j) x = {x} := by
…

theorem OAI.CircleDomainRigidity.component_lower_grid_union_dust_eq_singleton line 70

Source documentation

Adjoining dust creates no nondegenerate component through such a point. The assertion also covers points absent from every lower grid.

theorem component_lower_grid_union_dust_eq_singleton
    {X I J : Type*} [TopologicalSpace X] [CompactSpace X] [T2Space X]
    [Fintype I] [Fintype J] [Nonempty J]
    (H : I → J → Set X) (hH : ∀ i j, IsClosed (H i j))
    {B : Set X} (hB : IsClosed B) (hTD : IsTotallyDisconnected B)
    {x : X} (hxB : x ∈ B)
    (hunique : ∀ i j k, x ∈ H i j → x ∈ H i k → j = k)
    (hcompat : ∀ (A : Finset I) (k : I → J),
      ¬ (connectedComponentIn (⋃ i ∈ A, H i (k i)) x).Nontrivial) :
    connectedComponentIn ((⋃ i, ⋃ j, H i j) ∪ B) x = {x} := by
…