max_neg_neg

Mathlib.Data.EReal.Inv

URI: https://scilib.ai/kg/mathlib#EReal.max_neg_neg

English

The negation of the maximum of two elements equals the negative of the minimum: max(-x,-y) = -min(x,y).

Русский

Отрицание максимума двух чисел равно отрицанию минимума: max(-x,-y) = -min(x,y).

LaTeX

$$$ \max(-x,-y) = -\min(x,y) $$$

Lean4

theorem max_neg_neg (x y : EReal) : max (-x) (-y) = -min x y := by rcases le_total x y with (h | h) <;> simp_all

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

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

Разделы

Аффилиация

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