toNNReal_mul — Mathlib

English

Multiplication is preserved by the ENNReal-to-NNReal map: (a · b).toNNReal = a.toNNReal · b.toNNReal.

Русский

Умножение сохраняется под отображением ENNReal → NNReal: (a · b).toNNReal = a.toNNReal · b.toNNReal.

LaTeX

$$$ (a \cdot b).\mathsf{toNNReal} = a.\mathsf{toNNReal} \cdot b.\mathsf{toNNReal} $$$

Lean4

@[simp]
theorem toNNReal_mul {a b : ℝ≥0∞} : (a * b).toNNReal = a.toNNReal * b.toNNReal :=
  WithTop.untopD_zero_mul a b

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