inv_strictAnti — Mathlib

English

The inverse map on ENNReal is strictly decreasing: if a < b then b⁻¹ < a⁻¹.

Русский

Обратная карта на ENNReal строго убывает: если a < b, то b⁻¹ < a⁻¹.

LaTeX

$$∀ a,b ∈ \mathbb{R}_{\ge 0}^{\infty}, a < b ⇒ b^{-1} < a^{-1}$$

Lean4

theorem inv_strictAnti : StrictAnti (Inv.inv : ℝ≥0∞ → ℝ≥0∞) :=
  by
  intro a b h
  lift a to ℝ≥0 using h.ne_top
  cases b; · simp
  rw [coe_lt_coe] at h
  rcases eq_or_ne a 0 with (rfl | ha); · simp [h]
  rw [← coe_inv h.ne_bot, ← coe_inv ha, coe_lt_coe]
  exact NNReal.inv_lt_inv ha h

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