English
For x,y ∈ EReal with hy: 0 ≤ y, we have (x − y).toENNReal = x.toENNReal − y.toENNReal.
Русский
Для x,y ∈ EReal с условием hy: 0 ≤ y выполняется (x − y).toENNReal = x.toENNReal − y.toENNReal.
LaTeX
$$$$ (x - y).toENNReal = x.toENNReal - y.toENNReal \,\text{(when } 0 \le y). $$$$
Lean4
theorem toENNReal_sub {x y : EReal} (hy : 0 ≤ y) : (x - y).toENNReal = x.toENNReal - y.toENNReal :=
by
induction x <;> induction y <;>
try { · simp_all [zero_tsub, ENNReal.sub_top]
}
rename_i x y
by_cases hxy : x ≤ y
· rw [toENNReal_of_nonpos <| sub_nonpos.mpr <| EReal.coe_le_coe_iff.mpr hxy]
exact (tsub_eq_zero_of_le <| toENNReal_le_toENNReal <| EReal.coe_le_coe_iff.mpr hxy).symm
· rw [toENNReal_of_ne_top (ne_of_beq_false rfl).symm, ← coe_sub, toReal_coe, ofReal_sub x (EReal.coe_nonneg.mp hy)]
simp
