Nested intersections of continua

A continuum is a nonempty compact connected set. This file proves the standard structural theorem about them: the intersection of a family of compact connected sets that is downward directed — any two members contain a third — is again compact and connected. Mathlib has the union counterpart, IsPreconnected.sUnion_directed, and Cantor's intersection theorem IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed, but not the preservation of connectedness under a directed intersection; this file supplies it.

It is written for TauCeti/Topology/ClusterSet.lean, where the boundary cluster set of a map is exhibited as such an intersection and is thereby a continuum — the first step of the Carathéodory boundary correspondence, layer L5 of the conformal-mapping roadmap.

Both hypotheses on the family are essential. Without directedness a circle and a secant line are two continua meeting in two points, a disconnected intersection. Without compactness the theorem fails even for a decreasing sequence: in ℝ × ℝ the closed connected sets (ℝ ×ˢ {0}) ∪ (ℝ ×ˢ {1}) ∪ (Ici n ×ˢ Icc 0 1) — two parallel lines bridged by a strip that recedes to infinity — intersect in the two lines, which are disconnected.

The argument

Suppose the intersection C splits: C ⊆ u ∪ v with u, v open, both meeting C, and C ∩ u ∩ v = ∅. Then C \ v and C \ u are disjoint nonempty compact sets, so in a Hausdorff space they have disjoint open neighbourhoods U and V, and C ⊆ U ∪ V. So U ∪ V is a neighbourhood of every point of C, and exists_subset_nhds_of_isCompact — any neighbourhood of the intersection of a directed family of compacts already contains one member — supplies a single t i covered by U ∪ V. That member meets both U and V — it contains C — so its connectedness forces U ∩ V to be nonempty, a contradiction.

Main results

• TauCeti.isPreconnected_iInter_of_directed — a directed intersection of compact preconnected sets is preconnected.
• TauCeti.isConnected_iInter_of_directed — the continuum form: a directed intersection of continua is a continuum.

References

• E. F. Collingwood and A. J. Lohwater, The Theory of Cluster Sets, Ch. 1.
• K. Kuratowski, Topology II, §47.

theorem TauCeti.isPreconnected_iInter_of_directed {X : Type u_1} [TopologicalSpace X] {ι : Type u_2} {t : ι → Set X} [T2Space X] [Nonempty ι] (htd : Directed (fun (x1 x2 : Set X) => x1 ⊇ x2) t) (htc : ∀ (i : ι), IsCompact (t i)) (htp : ∀ (i : ι), IsPreconnected (t i)) : IsPreconnected (⋂ (i : ι), t i)

A directed intersection of compact preconnected sets is preconnected. The family t is indexed by a nonempty type and directed downwards: any two members contain a third.

Both hypotheses on the family are needed; see the module docstring for the two counterexamples.

theorem TauCeti.isConnected_iInter_of_directed {X : Type u_1} [TopologicalSpace X] {ι : Type u_2} {t : ι → Set X} [T2Space X] [Nonempty ι] (htd : Directed (fun (x1 x2 : Set X) => x1 ⊇ x2) t) (htn : ∀ (i : ι), (t i).Nonempty) (htc : ∀ (i : ι), IsCompact (t i)) (htp : ∀ (i : ι), IsPreconnected (t i)) : IsConnected (⋂ (i : ι), t i)

A directed intersection of continua is a continuum. The nonemptiness of the intersection is Cantor's intersection theorem, and its connectedness is TauCeti.isPreconnected_iInter_of_directed.