abs_max_sub_max_le_abs — Mathlib

English

For additive groups, |min a b − min c d| ≤ max |a − c| |b − d|, derived from a related inequality.

Русский

Для групп с дополнительно: неравенство о min и max через разности.

LaTeX

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

Lean4

theorem abs_max_sub_max_le_abs (a b c : α) : |max a c - max b c| ≤ |a - b| := by
  simpa only [sub_self, abs_zero, max_eq_left (abs_nonneg (a - b))] using abs_max_sub_max_le_max a c b c

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