max_div_div_left'

Mathlib.Algebra.Order.Group.MinMax

URI: https://scilib.ai/kg/mathlib#max_div_div_left'

← MathLib Explorer

English

In a commutative ordered group, max(a/b, a/c) = a / min(b,c).

Русский

В коммутативной упорядоченной группе: max(a/b, a/c) = a / min(b,c).

LaTeX

$$$ \max\left( \frac{a}{b}, \frac{a}{c} \right) = \frac{a}{\min(b,c)} $$$

Lean4

@[to_additive max_sub_sub_left]
theorem max_div_div_left' (a b c : α) : max (a / b) (a / c) = a / min b c := by
  simp only [div_eq_mul_inv, max_mul_mul_left, max_inv_inv']

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

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

Разделы

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

Аффилиация

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