rat_inf_continuous_lemma — Mathlib

English

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

Русский

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

LaTeX

Lean4

theorem rat_inf_continuous_lemma {ε : α} {a₁ a₂ b₁ b₂ : α} :
    abs (a₁ - b₁) < ε → abs (a₂ - b₂) < ε → abs (a₁ ⊓ a₂ - b₁ ⊓ b₂) < ε := fun h₁ h₂ =>
  (abs_min_sub_min_le_max _ _ _ _).trans_lt (max_lt h₁ h₂)

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