English
There exists a canonical ring homomorphism from the extended natural numbers ℕ∞ into the nonnegative extended reals ℝ≥0∞, defined by applying the natural-number embedding to ENNReal. This map carries addition and multiplication and extends the usual embedding of ℕ into ℝ≥0∞.
Русский
Существует каноническое кольцевое отображение из расширенных натуральных чисел ℕ∞ в ℝ≥0∞, задаваемое естественным встраиванием чисел. Это отображение сохраняет сложение и умножение и расширяет обычное внедрение ℕ в ℝ≥0∞.
LaTeX
$$$\\exists \\varphi: \\mathbb{N}_\\infty \\to \\mathbb{R}_{\\ge 0,\\infty} \\\\ (\\varphi\\text{ является кольцевым гомоморфизмом}) \\\\ \\varphi(n) = n\\quad(\\forall n \\in \\mathbb{N}).$$$
Lean4
/-- Coercion `ℕ∞ → ℝ≥0∞` as a ring homomorphism. -/
@[simps! -fullyApplied]
def toENNRealRingHom : ℕ∞ →+* ℝ≥0∞ :=
.ENatMap (Nat.castRingHom ℝ≥0) Nat.cast_injective
