English
The map ENNReal.toNNReal defines a MonoidWithZero hom from ENNReal to NNReal, sending the ENNReal structure to the NNReal structure.
Русский
Отображение ENNReal.toNNReal задаёт морфизм MonoidWithZero из ENNReal в NNReal, сохраняющий структуру умножения и единицу.
LaTeX
$$$\text{toNNRealHom} : \mathbb{R}_{\ge 0}^{\infty} \to_*^0 \mathbb{R}_{\ge 0}$$$
Lean4
/-- `ENNReal.toNNReal` as a `MonoidHom`. -/
def toNNRealHom : ℝ≥0∞ →*₀ ℝ≥0 where
toFun := ENNReal.toNNReal
map_one' := toNNReal_coe _
map_mul' _ _ := toNNReal_mul
map_zero' := toNNReal_zero