abs_min_sub_min_le_max — Mathlib

English

For any α-ordered additive group, |max(a,c) − max(b,d)| ≤ |a − b| ∨ |c − d|.

Русский

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

LaTeX

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

Lean4

theorem abs_min_sub_min_le_max (a b c d : α) : |min a b - min c d| ≤ max |a - c| |b - d| := by
  simpa only [max_neg_neg, neg_sub_neg, abs_sub_comm] using abs_max_sub_max_le_max (-a) (-b) (-c) (-d)

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