strictAnti_div_right_of_neg — Mathlib

English

If b < 0 and b ≠ ⊥, then a ↦ a / b is strictly anti-monotone.

Русский

Если b < 0 и b ≠ ⊥, то a ↦ a / b является строго антимонотонной по a.

LaTeX

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

Lean4

theorem strictAnti_div_right_of_neg (h : b < 0) (h' : b ≠ ⊥) : StrictAnti fun a ↦ a / b :=
  by
  intro a a' a_lt_a'
  simp only
  apply lt_of_le_of_ne <| div_le_div_right_of_nonpos (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 h' (ne_top_of_lt h) (ne_of_lt h), ← hyp,
    @EReal.mul_div_cancel a' b h' (ne_top_of_lt h) (ne_of_lt h)]

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