English
A total map on a complete space can be obtained from a vanishing-diameter, closed-antitone Cantor scheme with nonempty branches, yielding a unified map.
Русский
Схема Кантора с исчезающим диаметром и замыканием образует полный отображение, если ветви непустые.
LaTeX
$$$ (inducedMap A).1 = \mathrm{univ} \quad \text{under suitable hypotheses}. $$$
Lean4
/-- A scheme on a complete space with vanishing diameter
such that each set contains the closure of its children
induces a total map. -/
theorem map_of_vanishingDiam [CompleteSpace α] (hdiam : VanishingDiam A) (hanti : ClosureAntitone A)
(hnonempty : ∀ l, (A l).Nonempty) : (inducedMap A).1 = univ :=
by
rw [eq_univ_iff_forall]
intro x
choose u hu using fun n => hnonempty (res x n)
have umem : ∀ n m : ℕ, n ≤ m → u m ∈ A (res x n) :=
by
have : Antitone fun n : ℕ => A (res x n) :=
by
refine antitone_nat_of_succ_le ?_
intro n
apply hanti.antitone
intro n m hnm
exact this hnm (hu _)
have : CauchySeq u := by
rw [Metric.cauchySeq_iff]
intro ε ε_pos
obtain ⟨n, hn⟩ := hdiam.dist_lt _ ε_pos x
use n
intro m₀ hm₀ m₁ hm₁
apply hn <;> apply umem <;> assumption
obtain ⟨y, hy⟩ := cauchySeq_tendsto_of_complete this
use y
rw [mem_iInter]
intro n
apply hanti _ (x n)
apply mem_closure_of_tendsto hy
rw [eventually_atTop]
exact ⟨n.succ, umem _⟩
