min_div_div_right

Mathlib.Algebra.Order.Field.Basic

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

English

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

Русский

При c ≥ 0 выполняется min(a/c, b/c) = min(a, b)/c.

LaTeX

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

Lean4

theorem min_div_div_right {c : α} (hc : 0 ≤ c) (a b : α) : min (a / c) (b / c) = min a b / c :=
  (monotone_div_right_of_nonneg hc).map_min.symm

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

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

Разделы

Аффилиация

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