toENNReal_add — Mathlib

English

If x, y ≥ 0 in EReal, then (x + y).toENNReal = x.toENNReal + y.toENNReal.

Русский

Если x, y \\\\ge 0 в EReal, тогда (x+y).toENNReal = x.toENNReal + y.toENNReal.

LaTeX

$$$\\\\forall {x,y \\\\in \\\\mathrm{EReal}},\\\\ x \\\\ge 0 \\\\land y \\\\ge 0 \\\\Rightarrow (x+y).toENNReal = x.toENNReal + y.toENNReal$$$

Lean4

theorem toENNReal_add {x y : EReal} (hx : 0 ≤ x) (hy : 0 ≤ y) : (x + y).toENNReal = x.toENNReal + y.toENNReal :=
  by
  induction x <;> induction y <;>
    try { · simp_all
    }
  norm_cast
  simp_rw [real_coe_toENNReal]
  simp_all [ENNReal.ofReal_add]

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