English
For rationals with an absolute value, sums are continuous in the sense that for any epsilon > 0 there exists a delta > 0 such that a small change in summands yields a controlled change in the sum.
Русский
Для рациональных точек с модулем несложно показывается непрерывность суммы: при заданном ε существует δ, чтобы малые изменения входа приводили к контролируемому изменению суммы.
LaTeX
$$$\exists \delta>0\;\forall \{a_1,a_2,b_1,b_2\},\ abv(a_1-b_1)<\delta \land abv(a_2-b_2)<\delta \Rightarrow abv(a_1+a_2-b_1-b_2)<\epsilon$$$
Lean4
/-- A sequence is Cauchy if the distance between its entries tends to zero. -/
@[nolint unusedArguments]
def IsCauSeq {α : Type*} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {β : Type*} [Ring β] (abv : β → α)
(f : ℕ → β) : Prop :=
∀ ε > 0, ∃ i, ∀ j ≥ i, abv (f j - f i) < ε
