monotone_div_right_of_nonneg

Mathlib.Data.EReal.Inv

URI: https://scilib.ai/kg/mathlib#EReal.monotone_div_right_of_nonneg

English

If b ≥ 0, then the map a ↦ a / b is monotone in a.

Русский

Если b неотрицательно, то отображение a ↦ a / b по a монотонно не возрастает.

LaTeX

$$$0 \le b \Rightarrow \text{Monotone}(a \mapsto a / b)$$$

Lean4

theorem monotone_div_right_of_nonneg (h : 0 ≤ b) : Monotone fun a ↦ a / b := fun _ _ h' ↦
  mul_le_mul_of_nonneg_right h' (inv_nonneg_of_nonneg h)

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

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

Разделы

Аффилиация

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