antitone_div_right_of_nonpos — Mathlib

English

If b ≤ 0, then a ↦ a / b is antitone.

Русский

Если b ≤ 0, тогда a ↦ a / b является антимонотонной функцией по a.

LaTeX

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

Lean4

theorem antitone_div_right_of_nonpos (h : b ≤ 0) : Antitone fun a ↦ a / b :=
  by
  intro a a' h'
  change a' * b⁻¹ ≤ a * b⁻¹
  rw [← neg_neg (a * b⁻¹), ← neg_neg (a' * b⁻¹), neg_le_neg_iff, mul_comm a b⁻¹, mul_comm a' b⁻¹, ← neg_mul b⁻¹ a, ←
    neg_mul b⁻¹ a', mul_comm (-b⁻¹) a, mul_comm (-b⁻¹) a', ← inv_neg b]
  have : 0 ≤ -b := by apply EReal.le_neg_of_le_neg; simp [h]
  exact div_le_div_right_of_nonneg this h'

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