English
A space is complete if whenever sequences are controlled by a bound B(N) and a converging subsequence exists under that bound, the sequence converges.
Русский
Пространство полное, если любые последовательности, управляемые ограничением B(N), сходятся по такой схеме.
LaTeX
$$$\forall B: \mathbb{N} \to \mathbb{R}_{+}, \; (\forall n, B(n) > 0) \to \big( (\forall u: \mathbb{N} \, \to \\alpha, (\forall N,n,m, N\le n, N\le m \Rightarrow edist(u(n),u(m)) < B(N)) \Rightarrow \exists x, Tendsto u\!\to_{\infty} x) \Rightarrow \text{CompleteSpace}(\alpha).$$$
Lean4
/-- ε-δ characterization of Cauchy sequences on pseudoemetric spaces -/
protected theorem cauchy_iff {f : Filter α} :
Cauchy f ↔ f ≠ ⊥ ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x, x ∈ t → ∀ y, y ∈ t → edist x y < ε := by rw [← neBot_iff];
exact uniformity_basis_edist.cauchy_iff
