English
If (t_n) is a decreasing sequence of nonempty compact closed subsets of X (t_{n+1} ⊆ t_n) and each t_n is nonempty, compact, and closed, then the intersection over all n is nonempty: ⋂_{n} t_n ≠ ∅.
Русский
Если (t_n) — убывающая последовательность непустых компактно-замкнутых подмножеств X (t_{n+1} ⊆ t_n), и каждый t_n непуст, компактен и замкнуть, то пересечение по всем n непуcто: ⋂_n t_n ≠ ∅.
LaTeX
$$$\\\\bigcap_{n=0}^{\\infty} t_n \\\\neq \\\\emptyset$$$
Lean4
/-- Cantor's intersection theorem for sequences indexed by `ℕ`:
the intersection of a decreasing sequence of nonempty compact closed sets is nonempty. -/
theorem nonempty_iInter_of_sequence_nonempty_isCompact_isClosed (t : ℕ → Set X) (htd : ∀ i, t (i + 1) ⊆ t i)
(htn : ∀ i, (t i).Nonempty) (ht0 : IsCompact (t 0)) (htcl : ∀ i, IsClosed (t i)) : (⋂ i, t i).Nonempty :=
have tmono : Antitone t := antitone_nat_of_succ_le htd
have htd : Directed (· ⊇ ·) t := tmono.directed_ge
have : ∀ i, t i ⊆ t 0 := fun i => tmono <| Nat.zero_le i
have htc : ∀ i, IsCompact (t i) := fun i => ht0.of_isClosed_subset (htcl i) (this i)
IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed t htd htn htc htcl
