mk_left_le_mk_mul

Mathlib.Algebra.Order.Archimedean.Class

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

English

The same inequality for the division case with mk a and mk b.

Русский

Та же неравенство для случая деления с mk a и mk b.

LaTeX

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

Lean4

@[to_additive]
theorem mk_left_le_mk_mul (hab : mk a ≤ mk b) : mk a ≤ mk (a * b) := by
  simpa [hab] using min_le_mk_mul (a := a) (b := b)

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

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

Разделы

Аффилиация

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