strictMono_div_right_of_pos — Mathlib

English

If 0 < b and b ≠ ⊤, then a ↦ a / b is strictly monotone in a.

Русский

Если 0 < b и b ≠ ⊤, то функция a ↦ a / b строго монотонна по a.

LaTeX

$$$0 < b \land b \neq \top \Rightarrow \text{StrictMono}(a \mapsto a / b)$$$

Lean4

theorem strictMono_div_right_of_pos (h : 0 < b) (h' : b ≠ ⊤) : StrictMono fun a ↦ a / b :=
  by
  intro a a' a_lt_a'
  apply lt_of_le_of_ne <| div_le_div_right_of_nonneg (le_of_lt h) (le_of_lt a_lt_a')
  intro hyp
  apply ne_of_lt a_lt_a'
  rw [← @EReal.mul_div_cancel a b (ne_bot_of_gt h) h' (ne_of_gt h), hyp,
    @EReal.mul_div_cancel a' b (ne_bot_of_gt h) h' (ne_of_gt h)]

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