doc-next-gen

Mathlib.SetTheory.Cardinal.ToNat

Module docstring

{"# Projection from cardinal numbers to natural numbers

In this file we define Cardinal.toNat to be the natural projection Cardinal → ℕ, sending all infinite cardinals to zero. We also prove basic lemmas about this definition. "}

Cardinal.toNat definition
: Cardinal →*₀ ℕ
Full source 
/-- This function sends finite cardinals to the corresponding natural, and infinite cardinals
  to 0. -/
noncomputable def toNat : CardinalCardinal →*₀ ℕ :=
  ENat.toNatHom.comp toENat
Projection from cardinals to natural numbers (infinite ↦ 0)
Informal description
The function maps a cardinal number to a natural number by first converting it to an extended natural number (where infinite cardinals become $\infty$) and then applying the homomorphism that sends $\infty$ to $0$ and preserves finite natural numbers. In other words, it sends finite cardinals to their corresponding natural number and infinite cardinals to $0$.
Cardinal.toNat_toENat theorem
(a : Cardinal) : ENat.toNat (toENat a) = toNat a
Full source 
@[simp] lemma toNat_toENat (a : Cardinal) : ENat.toNat (toENat a) = toNat a := rfl
Commutativity of Cardinal Projection via Extended Naturals
Informal description
For any cardinal number $a$, the natural number obtained by first converting $a$ to an extended natural number and then applying the `ENat.toNat` function is equal to the natural number obtained by directly applying the `Cardinal.toNat` function to $a$. In other words, the following diagram commutes: $$\text{ENat.toNat} \circ \text{toENat} = \text{toNat}$$
Cardinal.toNat_ofENat theorem
(n : ℕ∞) : toNat n = ENat.toNat n
Full source 
@[simp]
theorem toNat_ofENat (n : ℕ∞) : toNat n = ENat.toNat n :=
  congr_arg ENat.toNat <| toENat_ofENat n
Equality of Cardinal and Extended Natural Number Projections to $\mathbb{N}$
Informal description
For any extended natural number $n \in \mathbb{N}_\infty$, the projection of $n$ to a natural number via `Cardinal.toNat` equals the projection via `ENat.toNat`, i.e., $\text{toNat}(n) = \text{ENat.toNat}(n)$.
Cardinal.toNat_natCast theorem
(n : ℕ) : toNat n = n
Full source 
@[simp, norm_cast] theorem toNat_natCast (n : ℕ) : toNat n = n := toNat_ofENat n
Projection of Natural Numbers Preserves Identity
Informal description
For any natural number $n$, the projection $\mathrm{toNat}(n)$ equals $n$.
Cardinal.toNat_eq_zero theorem
: toNat c = 0 ↔ c = 0 ∨ ℵ₀ ≤ c
Full source 
@[simp]
lemma toNat_eq_zero : toNattoNat c = 0 ↔ c = 0 ∨ ℵ₀ ≤ c := by
  rw [← toNat_toENat, ENat.toNat_eq_zero, toENat_eq_zero, toENat_eq_top]
Zero Projection Condition for Cardinal to Natural Number: $\mathrm{toNat}(c) = 0 \leftrightarrow c = 0 \lor \aleph_0 \leq c$
Informal description
For any cardinal number $c$, the projection $\mathrm{toNat}(c)$ equals zero if and only if $c$ is zero or $c$ is at least $\aleph_0$ (the first infinite cardinal).
Cardinal.toNat_ne_zero theorem
: toNat c ≠ 0 ↔ c ≠ 0 ∧ c < ℵ₀
Full source 
lemma toNat_ne_zero : toNattoNat c ≠ 0toNat c ≠ 0 ↔ c ≠ 0 ∧ c < ℵ₀ := by simp [not_or]
Nonzero Projection Condition for Cardinal to Natural Number: $\mathrm{toNat}(c) \neq 0 \leftrightarrow c \neq 0 \land c < \aleph_0$
Informal description
For any cardinal number $c$, the projection $\mathrm{toNat}(c)$ is nonzero if and only if $c$ is nonzero and strictly less than the first infinite cardinal $\aleph_0$.
Cardinal.toNat_pos theorem
: 0 < toNat c ↔ c ≠ 0 ∧ c < ℵ₀
Full source 
@[simp] lemma toNat_pos : 0 < toNat c ↔ c ≠ 0 ∧ c < ℵ₀ := pos_iff_ne_zero.trans toNat_ne_zero
Positivity of Cardinal-to-Natural Projection: $0 < \mathrm{toNat}(c) \leftrightarrow c \neq 0 \land c < \aleph_0$
Informal description
For any cardinal number $c$, the projection $\mathrm{toNat}(c)$ is strictly positive if and only if $c$ is nonzero and strictly less than the first infinite cardinal $\aleph_0$, i.e., $0 < \mathrm{toNat}(c) \leftrightarrow c \neq 0 \land c < \aleph_0$.
Cardinal.cast_toNat_of_lt_aleph0 theorem
{c : Cardinal} (h : c < ℵ₀) : ↑(toNat c) = c
Full source 
theorem cast_toNat_of_lt_aleph0 {c : Cardinal} (h : c < ℵ₀) : ↑(toNat c) = c := by
  lift c to ℕ using h
  rw [toNat_natCast]
Embedding of Finite Cardinals via toNat: $\mathrm{toNat}(c) = c$ for $c < \aleph_0$
Informal description
For any cardinal number $c$ such that $c < \aleph_0$, the canonical embedding of the natural number $\mathrm{toNat}(c)$ into the cardinals equals $c$, i.e., $\mathrm{toNat}(c) = c$.
Cardinal.toNat_apply_of_lt_aleph0 theorem
{c : Cardinal.{u}} (h : c < ℵ₀) : toNat c = Classical.choose (lt_aleph0.1 h)
Full source 
theorem toNat_apply_of_lt_aleph0 {c : CardinalCardinal.{u}} (h : c < ℵ₀) :
    toNat c = Classical.choose (lt_aleph0.1 h) :=
  Nat.cast_injective (R := CardinalCardinal.{u}) <| by
    rw [cast_toNat_of_lt_aleph0 h, ← Classical.choose_spec (lt_aleph0.1 h)]
Projection of Finite Cardinals via Axiom of Choice: $\mathrm{toNat}(c) = \text{choice}(c < \aleph_0)$
Informal description
For any cardinal number $c$ such that $c < \aleph_0$, the projection $\mathrm{toNat}(c)$ equals the natural number obtained by applying the axiom of choice to the proof that $c$ is finite (i.e., $\mathrm{toNat}(c) = \text{Classical.choose} (\text{lt\_aleph0.1 } h)$).
Cardinal.toNat_apply_of_aleph0_le theorem
{c : Cardinal} (h : ℵ₀ ≤ c) : toNat c = 0
Full source 
theorem toNat_apply_of_aleph0_le {c : Cardinal} (h : ℵ₀ ≤ c) : toNat c = 0 := by simp [h]
Projection of Infinite Cardinals to Zero
Informal description
For any cardinal number $c$ such that $\aleph_0 \leq c$, the projection of $c$ to natural numbers is zero, i.e., $\mathrm{toNat}(c) = 0$.
Cardinal.cast_toNat_of_aleph0_le theorem
{c : Cardinal} (h : ℵ₀ ≤ c) : ↑(toNat c) = (0 : Cardinal)
Full source 
theorem cast_toNat_of_aleph0_le {c : Cardinal} (h : ℵ₀ ≤ c) : ↑(toNat c) = (0 : Cardinal) := by
  rw [toNat_apply_of_aleph0_le h, Nat.cast_zero]
Embedding of Projection of Infinite Cardinals to Zero Cardinal
Informal description
For any cardinal number $c$ such that $\aleph_0 \leq c$, the canonical embedding of the natural number projection of $c$ into the cardinals equals the zero cardinal, i.e., $\mathrm{toNat}(c) = 0$ implies $\mathrm{toNat}(c) = 0$ in the cardinal numbers.
Cardinal.cast_toNat_eq_iff_lt_aleph0 theorem
{c : Cardinal} : (toNat c) = c ↔ c < ℵ₀
Full source 
theorem cast_toNat_eq_iff_lt_aleph0 {c : Cardinal} : (toNat c) = c ↔ c < ℵ₀ := by
  constructor
  · intro h; by_contra h'; rw [not_lt] at h'
    rw [toNat_apply_of_aleph0_le h'] at h; rw [← h] at h'
    absurd h'; rw [not_le]; exact nat_lt_aleph0 0
  · exact fun h ↦ (Cardinal.cast_toNat_of_lt_aleph0 h)
Finite Cardinal Embedding Criterion: $\mathrm{toNat}(c) = c$ iff $c < \aleph_0$
Informal description
For any cardinal number $c$, the canonical embedding of the natural number $\mathrm{toNat}(c)$ into the cardinals equals $c$ if and only if $c$ is finite, i.e., $c < \aleph_0$. In other words, $\mathrm{toNat}(c) = c$ holds precisely when $c$ is a finite cardinal.
Cardinal.toNat_strictMonoOn theorem
: StrictMonoOn toNat (Iio ℵ₀)
Full source 
theorem toNat_strictMonoOn : StrictMonoOn toNat (Iio ℵ₀) := by
  simp only [← range_natCast, StrictMonoOn, forall_mem_range, toNat_natCast, Nat.cast_lt]
  exact fun _ _ ↦ id
Strict Monotonicity of Cardinal-to-Natural Projection Below $\aleph_0$
Informal description
The projection function $\mathrm{toNat}$ from cardinal numbers to natural numbers is strictly increasing on the set of cardinals less than $\aleph_0$. That is, for any two cardinals $c_1, c_2 < \aleph_0$, if $c_1 < c_2$ then $\mathrm{toNat}(c_1) < \mathrm{toNat}(c_2)$.
Cardinal.toNat_monotoneOn theorem
: MonotoneOn toNat (Iio ℵ₀)
Full source 
theorem toNat_monotoneOn : MonotoneOn toNat (Iio ℵ₀) := toNat_strictMonoOn.monotoneOn
Monotonicity of Cardinal-to-Natural Projection Below $\aleph_0$
Informal description
The projection function $\mathrm{toNat}$ from cardinal numbers to natural numbers is monotone on the set of cardinals less than $\aleph_0$. That is, for any two cardinals $c_1, c_2 < \aleph_0$, if $c_1 \leq c_2$ then $\mathrm{toNat}(c_1) \leq \mathrm{toNat}(c_2)$.
Cardinal.toNat_injOn theorem
: InjOn toNat (Iio ℵ₀)
Full source 
theorem toNat_injOn : InjOn toNat (Iio ℵ₀) := toNat_strictMonoOn.injOn
Injectivity of Cardinal-to-Natural Projection Below $\aleph_0$
Informal description
The projection function $\mathrm{toNat}$ from cardinal numbers to natural numbers is injective on the set of cardinals less than $\aleph_0$. That is, for any two cardinals $c_1, c_2 < \aleph_0$, if $\mathrm{toNat}(c_1) = \mathrm{toNat}(c_2)$ then $c_1 = c_2$.
Cardinal.toNat_inj_of_lt_aleph0 theorem
(hc : c < ℵ₀) (hd : d < ℵ₀) : toNat c = toNat d ↔ c = d
Full source 
/-- Two finite cardinals are equal
iff they are equal their `Cardinal.toNat` projections are equal. -/
theorem toNat_inj_of_lt_aleph0 (hc : c < ℵ₀) (hd : d < ℵ₀) :
    toNattoNat c = toNat d ↔ c = d :=
  toNat_injOn.eq_iff hc hd
Injectivity of Cardinal-to-Natural Projection for Finite Cardinals
Informal description
For any finite cardinal numbers $c$ and $d$ (i.e., $c < \aleph_0$ and $d < \aleph_0$), the equality $\mathrm{toNat}(c) = \mathrm{toNat}(d)$ holds if and only if $c = d$.
Cardinal.toNat_le_iff_le_of_lt_aleph0 theorem
(hc : c < ℵ₀) (hd : d < ℵ₀) : toNat c ≤ toNat d ↔ c ≤ d
Full source 
theorem toNat_le_iff_le_of_lt_aleph0 (hc : c < ℵ₀) (hd : d < ℵ₀) :
    toNattoNat c ≤ toNat d ↔ c ≤ d :=
  toNat_strictMonoOn.le_iff_le hc hd
Order Preservation of Cardinal-to-Natural Projection Below $\aleph_0$: $\mathrm{toNat}(c) \leq \mathrm{toNat}(d) \leftrightarrow c \leq d$
Informal description
For any cardinal numbers $c$ and $d$ both less than $\aleph_0$, the projection $\mathrm{toNat}(c)$ is less than or equal to $\mathrm{toNat}(d)$ if and only if $c \leq d$.
Cardinal.toNat_lt_iff_lt_of_lt_aleph0 theorem
(hc : c < ℵ₀) (hd : d < ℵ₀) : toNat c < toNat d ↔ c < d
Full source 
theorem toNat_lt_iff_lt_of_lt_aleph0 (hc : c < ℵ₀) (hd : d < ℵ₀) :
    toNattoNat c < toNat d ↔ c < d :=
  toNat_strictMonoOn.lt_iff_lt hc hd
Cardinal-to-Natural Projection Preserves Strict Order Below $\aleph_0$
Informal description
For any cardinal numbers $c$ and $d$ such that $c < \aleph_0$ and $d < \aleph_0$, the inequality $\mathrm{toNat}(c) < \mathrm{toNat}(d)$ holds if and only if $c < d$.
Cardinal.toNat_le_toNat theorem
(hcd : c ≤ d) (hd : d < ℵ₀) : toNat c ≤ toNat d
Full source 
@[gcongr]
theorem toNat_le_toNat (hcd : c ≤ d) (hd : d < ℵ₀) : toNat c ≤ toNat d :=
  toNat_monotoneOn (hcd.trans_lt hd) hd hcd
Projection Preserves Order for Finite Cardinals
Informal description
For any cardinal numbers $c$ and $d$ such that $c \leq d$ and $d < \aleph_0$, the projection to natural numbers satisfies $\mathrm{toNat}(c) \leq \mathrm{toNat}(d)$.
Cardinal.toNat_lt_toNat theorem
(hcd : c < d) (hd : d < ℵ₀) : toNat c < toNat d
Full source 
theorem toNat_lt_toNat (hcd : c < d) (hd : d < ℵ₀) : toNat c < toNat d :=
  toNat_strictMonoOn (hcd.trans hd) hd hcd
Projection Preserves Strict Order for Finite Cardinals
Informal description
For any cardinal numbers $c$ and $d$ such that $c < d$ and $d < \aleph_0$, the projection to natural numbers satisfies $\mathrm{toNat}(c) < \mathrm{toNat}(d)$.
Cardinal.toNat_ofNat theorem
(n : ℕ) [n.AtLeastTwo] : Cardinal.toNat ofNat(n) = OfNat.ofNat n
Full source 
@[simp]
theorem toNat_ofNat (n : ℕ) [n.AtLeastTwo] :
    Cardinal.toNat ofNat(n) = OfNat.ofNat n :=
  toNat_natCast n
Projection of Embedded Natural Numbers Preserves Identity for $n \geq 2$
Informal description
For any natural number $n \geq 2$, the projection $\mathrm{toNat}$ applied to the canonical embedding of $n$ into cardinal numbers equals $n$.
Cardinal.toNat_rightInverse theorem
: Function.RightInverse ((↑) : ℕ → Cardinal) toNat
Full source 
/-- `toNat` has a right-inverse: coercion. -/
theorem toNat_rightInverse : Function.RightInverse ((↑) : ℕ → Cardinal) toNat :=
  toNat_natCast
Canonical Embedding is Right Inverse of Cardinal-to-Natural Projection
Informal description
The canonical embedding from natural numbers to cardinal numbers is a right inverse of the projection function $\mathrm{toNat} : \mathrm{Cardinal} \to \mathbb{N}$. That is, for any natural number $n$, we have $\mathrm{toNat}(n) = n$.
Cardinal.toNat_surjective theorem
: Surjective toNat
Full source 
theorem toNat_surjective : Surjective toNat :=
  toNat_rightInverse.surjective
Surjectivity of the Cardinal-to-Natural Projection
Informal description
The projection function $\mathrm{toNat} : \mathrm{Cardinal} \to \mathbb{N}$, which maps finite cardinals to their corresponding natural number and infinite cardinals to $0$, is surjective. That is, for every natural number $n$, there exists a cardinal number $\kappa$ such that $\mathrm{toNat}(\kappa) = n$.
Cardinal.mk_toNat_of_infinite theorem
[h : Infinite α] : toNat #α = 0
Full source 
@[simp]
theorem mk_toNat_of_infinite [h : Infinite α] : toNat #α = 0 := by simp
Projection of Infinite Cardinality to Natural Numbers is Zero
Informal description
For any infinite type $\alpha$, the projection of the cardinality of $\alpha$ to the natural numbers is zero, i.e., $\mathrm{toNat}(\#\alpha) = 0$.
Cardinal.aleph0_toNat theorem
: toNat ℵ₀ = 0
Full source 
@[simp]
theorem aleph0_toNat : toNat ℵ₀ = 0 :=
  toNat_apply_of_aleph0_le le_rfl
Projection of $\aleph_0$ to Natural Numbers is Zero
Informal description
The projection of the cardinal $\aleph_0$ to natural numbers is zero, i.e., $\mathrm{toNat}(\aleph_0) = 0$.
Cardinal.mk_toNat_eq_card theorem
[Fintype α] : toNat #α = Fintype.card α
Full source 
theorem mk_toNat_eq_card [Fintype α] : toNat #α = Fintype.card α := by simp
Projection of Finite Cardinality to Natural Numbers Preserves Cardinality
Informal description
For any finite type $\alpha$, the projection of the cardinality of $\alpha$ to natural numbers equals the cardinality of $\alpha$ as a finite type, i.e., $\mathrm{toNat}(\#\alpha) = \mathrm{card}(\alpha)$.
Cardinal.zero_toNat theorem
: toNat 0 = 0
Full source 
@[simp]
theorem zero_toNat : toNat 0 = 0 := map_zero _
Projection of zero cardinal to natural number is zero
Informal description
The projection of the zero cardinal to a natural number is zero, i.e., $\mathrm{toNat}(0) = 0$.
Cardinal.one_toNat theorem
: toNat 1 = 1
Full source 
theorem one_toNat : toNat 1 = 1 := map_one _
Projection of Cardinal One to Natural One: $\text{toNat}(1) = 1$
Informal description
The projection from cardinal numbers to natural numbers maps the cardinal number $1$ to the natural number $1$, i.e., $\text{toNat}(1) = 1$.
Cardinal.toNat_eq_iff theorem
{n : ℕ} (hn : n ≠ 0) : toNat c = n ↔ c = n
Full source 
theorem toNat_eq_iff {n : ℕ} (hn : n ≠ 0) : toNattoNat c = n ↔ c = n := by
  rw [← toNat_toENat, ENat.toNat_eq_iff hn, toENat_eq_nat]
Equivalence of Cardinal Projection and Equality for Nonzero Natural Numbers
Informal description
For any nonzero natural number $n$, the projection of a cardinal number $c$ to a natural number equals $n$ if and only if $c$ is equal to $n$. In other words, $\mathrm{toNat}(c) = n \leftrightarrow c = n$.
Cardinal.toNat_eq_ofNat theorem
{n : ℕ} [Nat.AtLeastTwo n] : toNat c = OfNat.ofNat n ↔ c = OfNat.ofNat n
Full source 
/-- A version of `toNat_eq_iff` for literals -/
theorem toNat_eq_ofNat {n : ℕ} [Nat.AtLeastTwo n] :
    toNattoNat c = OfNat.ofNat n ↔ c = OfNat.ofNat n :=
  toNat_eq_iff <| OfNat.ofNat_ne_zero n
Equivalence of Cardinal Projection and Equality for Natural Numbers $\geq 2$
Informal description
For any natural number $n \geq 2$, the projection of a cardinal number $c$ to a natural number equals $n$ if and only if $c$ is equal to $n$. In other words, $\mathrm{toNat}(c) = n \leftrightarrow c = n$.
Cardinal.toNat_eq_one_iff_unique theorem
: toNat #α = 1 ↔ Subsingleton α ∧ Nonempty α
Full source 
theorem toNat_eq_one_iff_unique : toNattoNat #α = 1 ↔ Subsingleton α ∧ Nonempty α :=
  toNat_eq_one.trans eq_one_iff_unique
Cardinality Projection to One Characterizes Unique Elements: $\mathrm{toNat}(\#\alpha) = 1 \leftrightarrow \text{Subsingleton } \alpha \land \text{Nonempty } \alpha$
Informal description
For any type $\alpha$, the projection of its cardinality to natural numbers equals $1$ if and only if $\alpha$ is a subsingleton (has at most one element) and is nonempty (has at least one element). In other words, $\mathrm{toNat}(\#\alpha) = 1 \leftrightarrow \text{Subsingleton } \alpha \land \text{Nonempty } \alpha$.
Cardinal.toNat_lift theorem
(c : Cardinal.{v}) : toNat (lift.{u, v} c) = toNat c
Full source 
@[simp]
theorem toNat_lift (c : CardinalCardinal.{v}) : toNat (lift.{u, v} c) = toNat c := by
  simp only [← toNat_toENat, toENat_lift]
Universe Lift Invariance of Cardinal-to-Natural Projection
Informal description
For any cardinal number $c$ in universe level $v$, the projection to natural numbers is preserved under universe lifting, i.e., $\mathrm{toNat}(\mathrm{lift}_{u,v}(c)) = \mathrm{toNat}(c)$.
Cardinal.toNat_congr theorem
{β : Type v} (e : α ≃ β) : toNat #α = toNat #β
Full source 
theorem toNat_congr {β : Type v} (e : α ≃ β) : toNat #α = toNat #β := by
  -- Porting note: Inserted universe hint below
  rw [← toNat_lift, (lift_mk_eq.{_,_,v}).mpr ⟨e⟩, toNat_lift]
Invariance of Cardinal-to-Natural Projection under Bijection
Informal description
For any types $\alpha$ and $\beta$ and a bijection $e : \alpha \simeq \beta$, the projection to natural numbers satisfies $\mathrm{toNat}(\#\alpha) = \mathrm{toNat}(\#\beta)$, where $\#\alpha$ denotes the cardinality of $\alpha$ and $\mathrm{toNat}$ maps finite cardinals to their corresponding natural numbers and infinite cardinals to $0$.
Cardinal.toNat_mul theorem
(x y : Cardinal) : toNat (x * y) = toNat x * toNat y
Full source 
theorem toNat_mul (x y : Cardinal) : toNat (x * y) = toNat x * toNat y := map_mul toNat x y
Multiplicativity of Cardinal-to-Natural-Number Projection
Informal description
For any cardinal numbers $x$ and $y$, the projection to natural numbers satisfies $\mathrm{toNat}(x \cdot y) = \mathrm{toNat}(x) \cdot \mathrm{toNat}(y)$, where $\mathrm{toNat}$ maps finite cardinals to their corresponding natural numbers and infinite cardinals to $0$.
Cardinal.toNat_add theorem
(hc : c < ℵ₀) (hd : d < ℵ₀) : toNat (c + d) = toNat c + toNat d
Full source 
@[simp]
theorem toNat_add (hc : c < ℵ₀) (hd : d < ℵ₀) : toNat (c + d) = toNat c + toNat d := by
  lift c to ℕ using hc
  lift d to ℕ using hd
  norm_cast
Additivity of Cardinal-to-Natural-Number Projection for Finite Cardinals
Informal description
For any finite cardinal numbers $c$ and $d$ (i.e., $c < \aleph_0$ and $d < \aleph_0$), the projection to natural numbers satisfies $\mathrm{toNat}(c + d) = \mathrm{toNat}(c) + \mathrm{toNat}(d)$.
Cardinal.toNat_lift_add_lift theorem
{a : Cardinal.{u}} {b : Cardinal.{v}} (ha : a < ℵ₀) (hb : b < ℵ₀) : toNat (lift.{v} a + lift.{u} b) = toNat a + toNat b
Full source 
@[simp]
theorem toNat_lift_add_lift {a : CardinalCardinal.{u}} {b : CardinalCardinal.{v}} (ha : a < ℵ₀) (hb : b < ℵ₀) :
    toNat (lift.{v} a + lift.{u} b) = toNat a + toNat b := by
  simp [*]
Additivity of Cardinal-to-Natural Projection under Universe Lifting for Finite Cardinals
Informal description
For any finite cardinal numbers $a$ in universe level $u$ and $b$ in universe level $v$ (i.e., $a < \aleph_0$ and $b < \aleph_0$), the projection to natural numbers satisfies $\mathrm{toNat}(\mathrm{lift}_{v}(a) + \mathrm{lift}_{u}(b)) = \mathrm{toNat}(a) + \mathrm{toNat}(b)$, where $\mathrm{lift}$ denotes universe lifting and $\mathrm{toNat}$ maps finite cardinals to their corresponding natural numbers and infinite cardinals to $0$.