English
For x ≥ 0, (x*y).toENNReal = x.toENNReal * y.toENNReal.
Русский
Для x ≥ 0 выполнено (x*y).toENNReal = x.toENNReal * y.toENNReal.
LaTeX
$$$ (x \cdot y).toENNReal = x.toENNReal * y.toENNReal \;\text{ при } 0 \le x$$$
Lean4
/-- `EReal.toENNReal` is multiplicative. For the version with the nonnegativity
hypothesis on the second variable, see `EReal.toENNReal_mul'`. -/
theorem toENNReal_mul {x y : EReal} (hx : 0 ≤ x) : (x * y).toENNReal = x.toENNReal * y.toENNReal :=
by
induction x <;> induction y <;>
try { · simp_all [mul_nonpos_iff, ofReal_mul, ← coe_mul]
}
· rcases eq_or_lt_of_le hx with (hx | hx)
· simp [← hx]
· simp_all [mul_top_of_pos hx]
· rename_i a
rcases lt_trichotomy a 0 with (ha | ha | ha)
· simp_all [le_of_lt, top_mul_of_neg (EReal.coe_neg'.mpr ha)]
· simp [ha]
· simp_all [top_mul_of_pos (EReal.coe_pos.mpr ha)]
