min_neg_neg

Mathlib.Data.EReal.Inv

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

English

The negation distributes over min: min(-x,-y) = -max(x,y).

Русский

Отрицание распределяется над минимумом: min(-x,-y) = -max(x,y).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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