English
A sequence of rationals is Cauchy (with respect to the absolute value) if and only if the corresponding real sequence is Cauchy.
Русский
Последовательность рациональних чисел является последовательностью Коши (по модулю) тогда и только тогда, когда соответствующая последовательность в ℝ также является последовательностью Коши.
LaTeX
$$$\mathrm{IsCauSeq}(\lvert \cdot \rvert, f) \iff \mathrm{IsCauSeq}(\lvert \cdot \rvert, i \mapsto (f(i) : \mathbb{R}))$$$
Lean4
theorem isCauSeq_iff_lift {f : ℕ → ℚ} : IsCauSeq abs f ↔ IsCauSeq abs fun i => (f i : ℝ)
where
mp H ε
ε0 :=
let ⟨δ, δ0, δε⟩ := exists_pos_rat_lt ε0
(H _ δ0).imp fun i hi j ij => by dsimp; exact lt_trans (mod_cast hi _ ij) δε
mpr H ε ε0 := (H _ (Rat.cast_pos.2 ε0)).imp fun i hi j ij => by dsimp at hi; exact mod_cast hi _ ij
