mul_div_le

Mathlib.Data.ENNReal.Inv

URI: https://scilib.ai/kg/mathlib#ENNReal.mul_div_le

English

For ENNReal, a*(b/a) ≤ b.

Русский

Для ENNReal выполняется a*(b/a) ≤ b.

LaTeX

$$$a \\cdot (b/a) \\le b$$$

Lean4

theorem mul_div_le : a * (b / a) ≤ b :=
  mul_le_of_le_div' le_rfl

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

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

Разделы

Аффилиация

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