min_div_div_left'

Mathlib.Algebra.Order.Group.MinMax

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive min_sub_sub_left]
theorem min_div_div_left' (a b c : α) : min (a / b) (a / c) = a / max b c := by
  simp only [div_eq_mul_inv, min_mul_mul_left, min_inv_inv']

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

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

Разделы

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

Аффилиация

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