abs_max_sub_max_le_max — Mathlib

English

For an ordered abelian group, |min(a,b) − min(c,d)| ≤ max(|a−c|,|b−d|).

Русский

Для упорядоченной абелевой группы: |min(a,b) − min(c,d)| ≤ max(|a−c|,|b−d|).

LaTeX

$$$ |\min(a,b) - \min(c,d)| \le \max\left(|a-c|, |b-d|\right) $$$

Lean4

theorem abs_max_sub_max_le_max (a b c d : α) : |max a b - max c d| ≤ max |a - c| |b - d| :=
  by
  refine abs_sub_le_iff.2 ⟨?_, ?_⟩
  · exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))
  · rw [abs_sub_comm a c, abs_sub_comm b d]
    exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))

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