enorm_ofReal_of_nonneg — Mathlib

English

Casting a nonnegative real a to ENNReal preserves the ENNorm: ‖ENNReal.ofReal a‖ₑ = ‖a‖ₑ.

Русский

Преобразование неотрицательного действительного a в ENNReal сохраняет ENNorm: ‖ENNReal.ofReal a‖ₑ = ‖a‖ₑ.

LaTeX

$$$$\|\mathrm{ofReal}(a)\|_{e} = \|a\|_{e} \quad (a \ge 0).$$$$

Lean4

theorem enorm_ofReal_of_nonneg {a : ℝ} (ha : 0 ≤ a) : ‖ENNReal.ofReal a‖ₑ = ‖a‖ₑ := by simp [Real.enorm_of_nonneg, ha]

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