English
There is a canonical ring homomorphism from NNReal to ENNReal sending a nonnegative real to its ENNReal embedding, i.e., the map r ↦ ↑r preserves addition and multiplication, and sends 0 to 0 and 1 to 1.
Русский
Существует каноническое кольцо-гомоморфизм NNReal в ENNReal, отображающий r ↦ ↑r; он сохраняет сложение и умножение и переводит 0 в 0 и 1 в 1.
LaTeX
$$$$ \text{ofNNRealHom} : \mathbb{R}_{\ge 0} \to^+* \mathbb{R}_{\ge 0}^{\infty}, \quad \operatorname{toFun}(r)=\uparrow r, \quad \text{map1} = \text{map0} = 0, \text{map1} = 1. $$$$
Lean4
/-- Coercion `ℝ≥0 → ℝ≥0∞` as a `RingHom`. -/
def ofNNRealHom : ℝ≥0 →+* ℝ≥0∞ where
toFun := WithTop.some
map_one' := coe_one
map_mul' _ _ := coe_mul _ _
map_zero' := coe_zero
map_add' _ _ := coe_add _ _
