max_div_div_right_of_nonpos

Mathlib.Algebra.Order.Field.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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