toNNReal_inv — Mathlib

English

Real.toNNReal respects inversion: Real.toNNReal x⁻¹ = (Real.toNNReal x)⁻¹ for all x ∈ ℝ.

Русский

Real.toNNReal сохраняет обращение: Real.toNNReal x⁻¹ = (Real.toNNReal x)⁻¹ для всех x ∈ ℝ.

LaTeX

$$$\forall x \in \mathbb{R},\ Real.toNNReal(x^{-1}) = (Real.toNNReal(x))^{-1}$$$

Lean4

theorem _root_.Real.toNNReal_inv {x : ℝ} : Real.toNNReal x⁻¹ = (Real.toNNReal x)⁻¹ :=
  by
  rcases le_total 0 x with hx | hx
  · nth_rw 1 [← Real.coe_toNNReal x hx]
    rw [← NNReal.coe_inv, Real.toNNReal_coe]
  · rw [toNNReal_eq_zero.mpr hx, inv_zero, toNNReal_eq_zero.mpr (inv_nonpos.mpr hx)]

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