ofReal_rpow_of_nonneg — Mathlib

English

For real x ≥ 0 and p ≥ 0, ENNReal.ofReal x ^ p = ENNReal.ofReal(x^p).

Русский

Для вещественного x ≥ 0 и p ≥ 0, ENNReal.ofReal x ^ p = ENNReal.ofReal(x^p).

LaTeX

$$$ (ENNReal.ofReal x)^p = ENNReal.ofReal (x^p) $$$

Lean4

theorem ofReal_rpow_of_nonneg {x p : ℝ} (hx_nonneg : 0 ≤ x) (hp_nonneg : 0 ≤ p) :
    ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p) :=
  by
  by_cases hp0 : p = 0
  · simp [hp0]
  by_cases hx0 : x = 0
  · rw [← Ne] at hp0
    have hp_pos : 0 < p := lt_of_le_of_ne hp_nonneg hp0.symm
    simp [hx0, hp_pos, hp_pos.ne.symm]
  rw [← Ne] at hx0
  exact ofReal_rpow_of_pos (hx_nonneg.lt_of_ne hx0.symm)

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