English
Let (s_n) be a sequence of subsets of a metric space X such that s_0 is complete, every s_n is closed and bounded, every finite intersection ⋂_{n≤N} s_n is nonempty, and diam(s_n) → 0. Then the infinite intersection ⋂_{n} s_n is nonempty.
Русский
Пусть (s_n) — последовательность подмножеств метрического пространства X; s_0 непусто и является полным множеством, каждое s_n замкнуто и ограничено, любое конечное пересечение ⋂_{n≤N} s_n непусто, и диаметр diam(s_n) сходится к 0. Тогда бесконечное пересечение ⋂_{n} s_n непусто.
LaTeX
$$$\text{Let } s: \mathbb{N} \to 2^{\alpha} \text{ with } s(0) \text{ complete}, \\ \forall n,\; \text{IsClosed}(s(n)), \; \forall n,\; \text{IsBounded}(s(n)), \\ \forall N,\; (\bigcap_{n\le N} s(n)).Nonempty, \\ \lim_{n\to\infty} \operatorname{diam}(s(n)) = 0 \\ \Rightarrow (\bigcap_{n} s(n)).Nonempty.$$$
Lean4
/-- If a family of complete sets with diameter tending to `0` is such that each finite intersection
is nonempty, then the total intersection is also nonempty. -/
theorem _root_.IsComplete.nonempty_iInter_of_nonempty_biInter {s : ℕ → Set α} (h0 : IsComplete (s 0))
(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 :=
by
let u N := (h N).some
have I : ∀ n N, n ≤ N → u N ∈ s n := by
intro n N hn
apply mem_of_subset_of_mem _ (h N).choose_spec
intro x hx
simp only [mem_iInter] at hx
exact hx n hn
have : CauchySeq u := by
apply cauchySeq_of_le_tendsto_0 _ _ h'
intro m n N hm hn
exact dist_le_diam_of_mem (h's N) (I _ _ hm) (I _ _ hn)
obtain ⟨x, -, xlim⟩ : ∃ x ∈ s 0, Tendsto (fun n : ℕ => u n) atTop (𝓝 x) :=
cauchySeq_tendsto_of_isComplete h0 (fun n => I 0 n (zero_le _)) this
refine ⟨x, mem_iInter.2 fun n => ?_⟩
apply (hs n).mem_of_tendsto xlim
filter_upwards [Ici_mem_atTop n] with p hp
exact I n p hp
