div_le_div

Mathlib.Data.ENNReal.Inv

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

← MathLib Explorer

English

If a ≤ b and c is ENNReal, then a/c ≤ b/c (monotonicity in numerator).

Русский

Если a ≤ b, то a/c ≤ b/c (монотонность по числителю).

LaTeX

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

Lean4

@[gcongr]
protected theorem div_le_div (hab : a ≤ b) (hdc : d ≤ c) : a / c ≤ b / d :=
  div_eq_mul_inv b d ▸ div_eq_mul_inv a c ▸ mul_le_mul' hab (ENNReal.inv_le_inv.mpr hdc)

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

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

Разделы

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

Аффилиация

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