min_le_mk_div

Mathlib.Algebra.Order.Archimedean.Class

URI: https://scilib.ai/kg/mathlib#MulArchimedeanClass.min_le_mk_div

← MathLib Explorer

English

The minimum of the Archimedean classes mk a and mk b is not greater than mk(a / b).

Русский

Минимум классов mk a и mk b не превосходит mk(a / b).

LaTeX

$$\min (mk a) (mk b) \le mk (a / b)$$

Lean4

@[to_additive]
theorem min_le_mk_div (a b : M) : min (mk a) (mk b) ≤ mk (a / b) := by
  simpa [div_eq_mul_inv] using min_le_mk_mul (a := a) (b := b⁻¹)

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

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

Разделы

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

Аффилиация

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