invENNReal — Mathlib

English

The map x ↦ x^{-1} is an order isomorphism between ENNReal and its order dual.

Русский

Отображение x ↦ x^{-1} задаёт изоморфизм порядка между ENNReal и его двойственным порядком.

LaTeX

$$$ invENNReal : ENNReal \cong_o ENNReal^{\mathrm{op}} $$$

Lean4

/-- The inverse map `fun x ↦ x⁻¹` is an order isomorphism between `ℝ≥0∞` and its `OrderDual` -/
@[simps! apply]
def _root_.OrderIso.invENNReal : ℝ≥0∞ ≃o ℝ≥0∞ᵒᵈ
    where
  map_rel_iff' := ENNReal.inv_le_inv
  toEquiv := (Equiv.inv ℝ≥0∞).trans OrderDual.toDual

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