toNNRealHom — Mathlib

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

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