rat_add_continuous_lemma — Mathlib

English

For any finite set s and any abv satisfying triangle inequality, abv(∑ f i) ≤ ∑ abv(f i).

Русский

Для любого конечного множества и абс. значения выполняется неравенство треугольника для сумм.

LaTeX

$$abv(\sum_{i∈s} f(i)) ≤ ∑_{i∈s} abv(f(i))$$

Lean4

theorem rat_add_continuous_lemma {ε : α} (ε0 : 0 < ε) :
    ∃ δ > 0, ∀ {a₁ a₂ b₁ b₂ : β}, abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ → abv (a₁ + a₂ - (b₁ + b₂)) < ε :=
  ⟨ε / 2, half_pos ε0, fun {a₁ a₂ b₁ b₂} h₁ h₂ => by
    simpa [add_halves, sub_eq_add_neg, add_comm, add_left_comm, add_assoc] using
      lt_of_le_of_lt (abv_add abv _ _) (add_lt_add h₁ h₂)⟩

Похожие утверждения