English
A space is complete if every Cauchy sequence has a limit; more exactly, if any function u: N → α that is Cauchy has a limit point, then α is complete.
Русский
Пространство полное, если любая последовательность Коши имеет предел; если любая функция u: N → α, являющаяся Коши, имеет предел, то пространство полно.
LaTeX
$$$ (\forall u: \mathbb{N} \to \alpha, CauchySeq(u) \Rightarrow \exists a, Tendsto(u, atTop, \mathcal{N}(a))) \Rightarrow \text{CompleteSpace}(\alpha). $$$
Lean4
/-- A very useful criterion to show that a space is complete is to show that all sequences
which satisfy a bound of the form `edist (u n) (u m) < B N` for all `n m ≥ N` are
converging. This is often applied for `B N = 2^{-N}`, i.e., with a very fast convergence to
`0`, which makes it possible to use arguments of converging series, while this is impossible
to do in general for arbitrary Cauchy sequences. -/
theorem complete_of_convergent_controlled_sequences (B : ℕ → ℝ≥0∞) (hB : ∀ n, 0 < B n)
(H : ∀ u : ℕ → α, (∀ N n m : ℕ, N ≤ n → N ≤ m → edist (u n) (u m) < B N) → ∃ x, Tendsto u atTop (𝓝 x)) :
CompleteSpace α :=
UniformSpace.complete_of_convergent_controlled_sequences (fun n => {p : α × α | edist p.1 p.2 < B n})
(fun n => edist_mem_uniformity <| hB n) H
