invENNReal_symm_apply — Mathlib

English

For all a in ENNReal^{op}, the inverse of the order isomorphism applied to a equals (OrderDual.ofDual a)^{-1}.

Русский

Для любого a из ENNReal^{op} применяемое к a обратное отображение порядка равно (OrderDual.ofDual a)^{-1}.

LaTeX

$$$ \mathrm{OrderIso.invENNReal}^{-1}(a) = ( \mathrm{OrderDual.ofDual}(a) )^{-1} $$$

Lean4

@[simp]
theorem _root_.OrderIso.invENNReal_symm_apply (a : ℝ≥0∞ᵒᵈ) : OrderIso.invENNReal.symm a = (OrderDual.ofDual a)⁻¹ :=
  rfl

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