English
In a complete space, if a family of closed sets with diameter tending to 0 has the finite intersection property (every finite intersection is nonempty) and each set is bounded, then the total intersection is nonempty.
Русский
В полном пространстве, если семейство замкнутых множества с диаметром, стремящимся к нулю, обладает свойством конечных пересечений (любое конечное пересечение непусто) и каждый набор ограничен, то их полное пересечение непусто.
LaTeX
$$$[CompleteSpace\ α]\; \{s_n\}_{n\in\mathbb{N}}:\;\text{IsClosed}(s_n),\; \text{IsBounded}(s_n),\; (\bigcap_{n\le N} s_n).Nonempty\text{ for all }N,\; \lim_{n\to\infty} \operatorname{diam}(s_n) = 0 \Longrightarrow (\bigcap_{n} s_n).Nonempty.$$$
Lean4
/-- In a complete space, if a family of closed sets with diameter tending to `0` is such that each
finite intersection is nonempty, then the total intersection is also nonempty. -/
theorem nonempty_iInter_of_nonempty_biInter [CompleteSpace α] {s : ℕ → Set α} (hs : ∀ n, IsClosed (s n))
(h's : ∀ n, IsBounded (s n)) (h : ∀ N, (⋂ n ≤ N, s n).Nonempty) (h' : Tendsto (fun n => diam (s n)) atTop (𝓝 0)) :
(⋂ n, s n).Nonempty :=
(hs 0).isComplete.nonempty_iInter_of_nonempty_biInter hs h's h h'
