theorem Real_Analysis.cauchy_seq_iff (x : ℕ → ℝ) : CauchySeq x ↔ ∀ ε > 0, ∃ (M : ℕ), ∀ (n k : ℕ), n ≥ M → k ≥ M → |x n - x k| < ε

A real sequence x is Cauchy (in the Mathlib sense, CauchySeq x) if and only if it satisfies the textbook Cauchy criterion: for every ε > 0 there exists M : ℕ such that |x n - x k| < ε whenever n, k ≥ M.

theorem Real_Analysis.cauchy_iff_convergent (x : ℕ → ℝ) : CauchySeq x ↔ ∃ (L : ℝ), Filter.Tendsto x Filter.atTop (nhds L)

Cauchy completeness of the reals: a real sequence is Cauchy if and only if it converges to some limit L : ℝ.