coe_ennreal_mul — Mathlib

English

The embedding preserves multiplication: (x*y) in ENNReal maps to (x:EReal) * y.

Русский

Вложение сохраняет умножение: (x*y) в ENNReal сопоставляется (x:EReal) * y.

LaTeX

$$$$ ((x * y) : ENNReal) = (x : EReal) * y, \quad x,y \in ENNReal. $$$$

Lean4

@[simp, norm_cast]
theorem coe_ennreal_mul : ∀ x y : ℝ≥0∞, ((x * y : ℝ≥0∞) : EReal) = (x : EReal) * y
  | ⊤, ⊤ => rfl
  | ⊤, (y : ℝ≥0) => coe_ennreal_top_mul y
  | (x : ℝ≥0), ⊤ => by rw [mul_comm, coe_ennreal_top_mul, EReal.mul_comm, coe_ennreal_top]
  | (x : ℝ≥0), (y : ℝ≥0) => by simp only [← ENNReal.coe_mul, coe_nnreal_eq_coe_real, NNReal.coe_mul, EReal.coe_mul]

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