ofReal_add — Mathlib

English

For nonnegative p,q ∈ ℝ, ENNReal.ofReal(p+q) = ENNReal.ofReal(p) + ENNReal.ofReal(q).

Русский

Для неотрицательных p,q ∈ ℝ: ENNReal.ofReal(p+q) = ENNReal.ofReal(p) + ENNReal.ofReal(q).

LaTeX

$$$\\text{ofReal}(p+q) = \\text{ofReal}(p) + \\text{ofReal}(q) \\quad (p,q\\in\\mathbb{R},\\ p,q\\ge 0)$$$

Lean4

theorem ofReal_add {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) : ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q :=
  by rw [ENNReal.ofReal, ENNReal.ofReal, ENNReal.ofReal, ← coe_add, coe_inj, Real.toNNReal_add hp hq]

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