NestedEndComponents.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Nested target collars and complementary components

The end-component argument uses compactness twice: a nested sequence of continua has connected intersection, and a connected subset of a finite disjoint closed cover stays in the piece containing its initial point. These are proved here for the actual target sphere. No uniformization or boundary-extension statement is assumed.

theorem OAI.CircleDomainRigidity.nested_sphere_sets_eventually_subset line 22
theorem OAI.CircleDomainRigidity.isConnected_nested_sphere_intersection line 30

theorem OAI.CircleDomainRigidity.connectedComponentIn_subset_finite_closed_piece line 52

Source documentation

A component of a subset of a finite disjoint closed union stays in the unique piece that contains the chosen point. The pieces need not themselves be connected.

theorem connectedComponentIn_subset_finite_closed_piece
    {I : Type*} [Finite I] {E : Set Sphere}
    (C : I → Set Sphere) (hC : ∀ i, IsClosed (C i))
    (hdisj : Pairwise (Disjoint on C)) (hcover : E ⊆ ⋃ i, C i)
    {i : I} {p : Sphere} (hp : p ∈ E) (hpi : p ∈ C i) :
    connectedComponentIn E p ⊆ C i := by
…

Mentions: OAI.CircleDomainRigidity.Sphere

theorem OAI.CircleDomainRigidity.connectedComponentIn_eq_nested_end line 81

Source documentation

The nested target disks for an end form exactly one complementary component once the finite image cores give the closed covers.

theorem connectedComponentIn_eq_nested_end
    {I : ℕ → Type*} [∀ n, Finite (I n)] {E : Set Sphere}
    (C : (n : ℕ) → I n → Set Sphere) (b : (n : ℕ) → I n)
    (hclosed : ∀ n i, IsClosed (C n i))
    (hconn : ∀ n, IsConnected (C n (b n)))
    (hdisj : ∀ n, Pairwise (Disjoint on C n))
    (hcover : ∀ n, E ⊆ ⋃ i, C n i)
    (hnest : Antitone (fun n => C n (b n)))
    (hmiss : (⋂ n, C n (b n)) ⊆ E)
    {p : Sphere} (hp : p ∈ ⋂ n, C n (b n)) :
    connectedComponentIn E p = ⋂ n, C n (b n) := by
…

Mentions: OAI.CircleDomainRigidity.Sphere

theorem OAI.CircleDomainRigidity.nested_end_subset_interior line 101
Source documentation
Strict nesting traps the limiting end inside every earlier collar.
```
theorem nested_end_subset_interior
    {C : ℕ → Set Sphere} (hstrict : ∀ n, C (n + 1) ⊆ interior (C n)) (n : ℕ) :
    (⋂ k, C k) ⊆ interior (C n) :=
…
```
Mentions: OAI.CircleDomainRigidity.Sphere