ofReal_inv_of_pos — Mathlib

English

Let x ∈ ℝ with x > 0. Then ENNReal.ofReal(x^{-1}) = (ENNReal.ofReal x)^{-1}.

Русский

Пусть x ∈ ℝ и x > 0. Тогда ENNReal.ofReal(x^{-1}) = (ENNReal.ofReal x)^{-1}.

LaTeX

$$$0 < x \Rightarrow ENNReal.ofReal(x^{-1}) = (ENNReal.ofReal x)^{-1}$$$

Lean4

@[simp]
theorem ofReal_inv_of_pos {x : ℝ} (hx : 0 < x) : ENNReal.ofReal x⁻¹ = (ENNReal.ofReal x)⁻¹ := by
  rw [ENNReal.ofReal, ENNReal.ofReal, ← @coe_inv (Real.toNNReal x) (by simp [hx]), coe_inj, ← Real.toNNReal_inv]

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