inv_lt_iff_inv_lt — Mathlib

English

The inverse map is strictly antitone, i.e., preserves the strict order in reverse.

Русский

Обратное отображение строго антимонотонно, т.е. обратное сохранение строгого порядка.

LaTeX

$$StrictAnti (Inv.inv : \mathbb{R}_{\ge 0}^{\infty} → \mathbb{R}_{\ge 0}^{\infty})$$

Lean4

theorem inv_lt_iff_inv_lt : a⁻¹ < b ↔ b⁻¹ < a := by simpa only [inv_inv] using @ENNReal.inv_lt_inv a b⁻¹

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