theorem bounded_of_antitone_base {X : Type u} [MetricSpace X] (C : ℕ → Set X) (hanti : Antitone C) (hbdd : Bornology.IsBounded (C 0)) (n : ℕ) : Bornology.IsBounded (C n)

Helper for Lemma 1.43: antitonicity pushes the boundedness of the initial set to every later set in the chain.

theorem finite_intersection_nonempty_of_antitone {X : Type u} [MetricSpace X] (C : ℕ → Set X) (hnonempty : ∀ (n : ℕ), (C n).Nonempty) (hanti : Antitone C) (N : ℕ) : (⋂ (n : ℕ), ⋂ (_ : n ≤ N), C n).Nonempty

Helper for Lemma 1.43: every finite intersection in an antitone nonempty family is nonempty.

theorem eq_of_mem_iInter_of_diam_tendsto_zero {X : Type u} [MetricSpace X] (C : ℕ → Set X) (hbounded : ∀ (n : ℕ), Bornology.IsBounded (C n)) (hdiam : Filter.Tendsto (Metric.diam ∘ C) Filter.atTop (nhds 0)) {x y : X} (hx : x ∈ ⋂ (n : ℕ), C n) (hy : y ∈ ⋂ (n : ℕ), C n) : x = y

Helper for Lemma 1.43: two points lying in all sets of the chain must coincide once the diameters converge to 0.

theorem exists_eq_singleton_iInter_of_nonempty_isClosed_antitone_diam_tendsto_zero {X : Type u} [MetricSpace X] [CompleteSpace X] (C : ℕ → Set X) (hnonempty : ∀ (n : ℕ), (C n).Nonempty) (hclosed : ∀ (n : ℕ), IsClosed (C n)) (hanti : Antitone C) (hbdd : Bornology.IsBounded (C 0)) (hdiam : Filter.Tendsto (Metric.diam ∘ C) Filter.atTop (nhds 0)) : ∃ (x : X), ⋂ (n : ℕ), C n = {x}

Lemma 1.43 (Cantor): in a complete metric space, a bounded antitone sequence of nonempty closed sets whose diameters converge to 0 has intersection equal to a singleton.

theorem exists_eq_singleton_iInter_of_nonempty_isClosed_succ_subset_diam_tendsto_zero {X : Type u} [MetricSpace X] [CompleteSpace X] (C : ℕ → Set X) (hnonempty : ∀ (n : ℕ), (C n).Nonempty) (hclosed : ∀ (n : ℕ), IsClosed (C n)) (hnest : ∀ (n : ℕ), C (n + 1) ⊆ C n) (hbdd : Bornology.IsBounded (C 0)) (hdiam : Filter.Tendsto (fun (n : ℕ) => Metric.diam (C n)) Filter.atTop (nhds 0)) : ∃ (x : X), ⋂ (n : ℕ), C n = {x}

Lemma 1.43 (Cantor), in the textbook successor-step formulation with bounded initial set.