max_sub_max_le_max

Mathlib.Algebra.Order.Group.MinMax

URI: https://scilib.ai/kg/mathlib#max_sub_max_le_max

English

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

Русский

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

LaTeX

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

Lean4

theorem max_sub_max_le_max (a b c d : α) : max a b - max c d ≤ max (a - c) (b - d) := by grind

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru