rat_sup_continuous_lemma — Mathlib

English

If |a1 - b1| < ε and |a2 - b2| < ε, then |max(a1,a2) - max(b1,b2)| < ε.

Русский

Если |a1 - b1| < ε и |a2 - b2| < ε, то |max(a1,a2) - max(b1,b2)| < ε.

LaTeX

Lean4

theorem rat_sup_continuous_lemma {ε : α} {a₁ a₂ b₁ b₂ : α} :
    abs (a₁ - b₁) < ε → abs (a₂ - b₂) < ε → abs (a₁ ⊔ a₂ - b₁ ⊔ b₂) < ε := fun h₁ h₂ =>
  (abs_max_sub_max_le_max _ _ _ _).trans_lt
    (max_lt h₁ h₂)
      -- so named to match `rat_add_continuous_lemma`

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