English
A uniform space is complete provided that (a) its uniformity has a countable basis and (b) any sequence that satisfies a controlled Cauchy condition converges.
Русский
Упорядоченное равномерное пространство является полным, если (a) у его равномерности счетная база, и (b) любая последовательность, удовлетворяющая контролируемому условию Коши, сходится.
LaTeX
$$$\text{CompleteSpace}(\alpha) \;\Longleftarrow\; \big( (\text{UniformSpace}\ α).\text{IsCountablyGenerated} \wedge (HU) \big)$$$
Lean4
/-- A sequentially complete uniform space with a countable basis of the uniformity filter is
complete. -/
theorem complete_of_cauchySeq_tendsto (H' : ∀ u : ℕ → α, CauchySeq u → ∃ a, Tendsto u atTop (𝓝 a)) : CompleteSpace α :=
let ⟨U', _, hU'⟩ := (𝓤 α).exists_antitone_seq
complete_of_convergent_controlled_sequences U' (fun n => hU'.2 ⟨n, Subset.refl _⟩) fun u hu =>
H' u <| cauchySeq_of_controlled U' (fun _ hs => hU'.1 hs) hu
