English
If for a pseudo-metric space α and a sequence of bounds B:N→ℝ with B_N>0, every sequence u:ℕ→α such that dist(u_n,u_m) < B_N for all N≤n,m has a limit, then α is a complete space.
Русский
Если для псевдометрик пространства α и последовательности границ B_n>0 каждая последовательность u:ℕ→α удовлетворяющая dist(u_n,u_m) < B_N для всех N≤n,m имеет предел, тогда α полно относительно метрики.
LaTeX
$$$\forall B: \mathbb{N} \to \mathbb{R},\; (\forall n, B(n) > 0) \to (\forall u: \mathbb{N} \to α, (\forall N n m, N \le n \to N \le m \to dist(u_n,u_m) < B(N)) \to \exists x, Tendsto u\ atTop \ (\mathcal{N}_x)).$$$
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 `dist (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 : ℕ → Real) (hB : ∀ n, 0 < B n)
(H : ∀ u : ℕ → α, (∀ N n m : ℕ, N ≤ n → N ≤ m → dist (u n) (u m) < B N) → ∃ x, Tendsto u atTop (𝓝 x)) :
CompleteSpace α :=
UniformSpace.complete_of_convergent_controlled_sequences (fun n => {p : α × α | dist p.1 p.2 < B n})
(fun n => dist_mem_uniformity <| hB n) H
