div_le_div_left

Mathlib.Data.ENNReal.Inv

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

English

For a ≤ b, dividing by the same ENNReal c preserves the inequality: a/c ≤ b/c.

Русский

При делении на одно и то же значение c неравенство сохраняется: a/c ≤ b/c.

LaTeX

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

Lean4

protected theorem div_le_div_left (h : a ≤ b) (c : ℝ≥0∞) : c / b ≤ c / a :=
  ENNReal.div_le_div le_rfl h

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

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

Разделы

Аффилиация

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