div_le_of_le_mul'

Mathlib.Data.ENNReal.Inv

URI: https://scilib.ai/kg/mathlib#ENNReal.div_le_of_le_mul'

English

If a ≤ b / c then a / b ≤ c.

Русский

Если a ≤ b / c, то a / b ≤ c.

LaTeX

$$ a \le \dfrac{b}{c} \implies \dfrac{a}{b} \le c $$

Lean4

theorem div_le_of_le_mul' (h : a ≤ b * c) : a / b ≤ c :=
  div_le_of_le_mul <| mul_comm b c ▸ h

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

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

Разделы

Аффилиация

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