max_div_div_right

Mathlib.Algebra.Order.Field.Basic

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

English

For c ≥ 0, max(a/c, b/c) = max(a,b)/c.

Русский

При c ≥ 0 верно max(a/c, b/c) = max(a,b)/c.

LaTeX

$$$c \ge 0 \Rightarrow \max\left(\frac{a}{c}, \frac{b}{c}\right) = \frac{\max(a,b)}{c}$$$

Lean4

theorem max_div_div_right {c : α} (hc : 0 ≤ c) (a b : α) : max (a / c) (b / c) = max a b / c :=
  (monotone_div_right_of_nonneg hc).map_max.symm

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

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

Разделы

Аффилиация

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