toRealHom — Mathlib

English

The map ENNReal.toReal is a MonoidWithZero hom from ENNReal to Real, obtained by composing ENNReal.toNNReal with NNReal.toReal.

Русский

Отображение ENNReal.toReal является моноидальным гомоморфизмом ENNReal → Real, полученным как композиция ENNReal.toNNReal и NNReal.toReal.

LaTeX

$$$\text{toRealHom} : \mathbb{R}_{\ge 0}^{\infty} \to_*^0 \mathbb{R}$$$

Lean4

/-- `ENNReal.toReal` as a `MonoidHom`. -/
def toRealHom : ℝ≥0∞ →*₀ ℝ :=
  (NNReal.toRealHom : ℝ≥0 →*₀ ℝ).comp toNNRealHom

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