min_div_div_right_of_nonpos

Mathlib.Algebra.Order.Field.Basic

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

← MathLib Explorer

English

If c ≤ 0, then min(a/c, b/c) = max(a,b)/c.

Русский

Если c ≤ 0, то min(a/c, b/c) = max(a,b)/c.

LaTeX

$$(hc : c \le 0) (a b : α) : min (a / c) (b / c) = max a b / c$$

Lean4

theorem min_div_div_right_of_nonpos (hc : c ≤ 0) (a b : α) : min (a / c) (b / c) = max a b / c :=
  Eq.symm <| Antitone.map_max fun _ _ => div_le_div_of_nonpos_of_le hc

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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