English
There is a natural-valued homomorphism from cardinals to natural numbers that sends finite cardinals to their natural numbers and infinite cardinals to 0.
Русский
Существует отображение кардиналов в натуральные числа, сохраняющее умножение и ноль, которое переводит конечные кардиналы в свои натуральные значения, а бесконечные кардиналы в 0.
LaTeX
$$$toNat: \mathrm{Cardinal} \to \mathbb{N}$ является моноидальным отображением в $\mathbb{N}$ и отправляет конечные кардиналы в их числа, а бесконечные — в 0.$$
Lean4
/-- This function sends finite cardinals to the corresponding natural, and infinite cardinals
to 0. -/
noncomputable def toNat : Cardinal →*₀ ℕ :=
ENat.toNatHom.comp toENat
