English
Let {t_i} be a directed family (with respect to reverse inclusion) of nonempty compact closed subsets of a topological space X. Then their intersection is nonempty: ⋂i t_i ≠ ∅.
Русский
Пусть {t_i} — направленная по отношению к обратному включению семья непустых компактно-замкнутых подмножеств пространства X. Тогда их пересечение не пусто: ⋂i t_i ≠ ∅.
LaTeX
$$$\\\\bigcap_i t_i \\\\neq \\\\emptyset$$$
Lean4
/-- Cantor's intersection theorem for `iInter`:
the intersection of a directed family of nonempty compact closed sets is nonempty. -/
theorem nonempty_iInter_of_directed_nonempty_isCompact_isClosed {ι : Type v} [hι : Nonempty ι] (t : ι → Set X)
(htd : Directed (· ⊇ ·) t) (htn : ∀ i, (t i).Nonempty) (htc : ∀ i, IsCompact (t i)) (htcl : ∀ i, IsClosed (t i)) :
(⋂ i, t i).Nonempty := by
let i₀ := hι.some
suffices (t i₀ ∩ ⋂ i, t i).Nonempty by rwa [inter_eq_right.mpr (iInter_subset _ i₀)] at this
simp only [nonempty_iff_ne_empty] at htn ⊢
apply mt ((htc i₀).elim_directed_family_closed t htcl)
push_neg
simp only [← nonempty_iff_ne_empty] at htn ⊢
refine ⟨htd, fun i => ?_⟩
rcases htd i₀ i with ⟨j, hji₀, hji⟩
exact (htn j).mono (subset_inter hji₀ hji)
