doc-next-gen

Mathlib.SetTheory.Cardinal.ENat

Module docstring

{"# Conversion between Cardinal and ℕ∞

In this file we define a coercion Cardinal.ofENat : ℕ∞ → Cardinal and a projection Cardinal.toENat : Cardinal →+*o ℕ∞. We also prove basic theorems about these definitions.

Implementation notes

We define Cardinal.ofENat as a function instead of a bundled homomorphism so that we can use it as a coercion and delaborate its application to ↑n.

We define Cardinal.toENat as a bundled homomorphism so that we can use all the theorems about homomorphisms without specializing them to this function. Since it is not registered as a coercion, the argument about delaboration does not apply.

Keywords

set theory, cardinals, extended natural numbers "}

Cardinal.ofENat definition
: ℕ∞ → Cardinal
Full source 
/-- Coercion `ℕ∞ → Cardinal`. It sends natural numbers to natural numbers and `⊤` to `ℵ₀`.

See also `Cardinal.ofENatHom` for a bundled homomorphism version. -/
@[coe] def ofENat : ℕ∞ → Cardinal
  | (n : ℕ) => n
  | ⊤ => ℵ₀
Embedding of extended natural numbers into cardinals
Informal description
The function maps an extended natural number $n \in \mathbb{N}_\infty$ to a cardinal number, where finite natural numbers are mapped to their corresponding finite cardinals and the infinity element $\top$ is mapped to the first infinite cardinal $\aleph_0$.
Cardinal.instCoeENat instance
: Coe ENat Cardinal
Full source 
instance : Coe ENat Cardinal := ⟨Cardinal.ofENat⟩
Coercion from Extended Natural Numbers to Cardinals
Informal description
There is a canonical coercion from the extended natural numbers $\mathbb{N}_\infty$ to the cardinal numbers, where finite natural numbers are mapped to their corresponding finite cardinals and $\infty$ is mapped to the first infinite cardinal $\aleph_0$.
Cardinal.ofENat_top theorem
: ofENat ⊤ = ℵ₀
Full source 
@[simp, norm_cast] lemma ofENat_top : ofENat ⊤ = ℵ₀ := rfl
$\text{ofENat}(\infty) = \aleph_0$
Informal description
The embedding of the extended natural numbers into cardinal numbers maps the infinity element $\top$ to the first infinite cardinal $\aleph_0$, i.e., $\text{ofENat}(\top) = \aleph_0$.
Cardinal.ofENat_nat theorem
(n : ℕ) : ofENat n = n
Full source 
@[simp, norm_cast] lemma ofENat_nat (n : ℕ) : ofENat n = n := rfl
Embedding of Natural Numbers Preserves Cardinality
Informal description
For any natural number $n$, the embedding of $n$ as an extended natural number into cardinal numbers equals $n$ as a cardinal number, i.e., $\text{ofENat}(n) = n$.
Cardinal.ofENat_zero theorem
: ofENat 0 = 0
Full source 
@[simp, norm_cast] lemma ofENat_zero : ofENat 0 = 0 := rfl
Embedding of Zero Extended Natural Number Yields Zero Cardinal
Informal description
The embedding of the extended natural number $0$ into cardinal numbers equals the zero cardinal, i.e., $\text{ofENat}(0) = 0$.
Cardinal.ofENat_one theorem
: ofENat 1 = 1
Full source 
@[simp, norm_cast] lemma ofENat_one : ofENat 1 = 1 := rfl
Embedding of One: $\text{ofENat}(1) = 1$
Informal description
The embedding of the extended natural number $1$ into cardinal numbers equals the cardinal number $1$, i.e., $\text{ofENat}(1) = 1$.
Cardinal.ofENat_ofNat theorem
(n : ℕ) [n.AtLeastTwo] : ((ofNat(n) : ℕ∞) : Cardinal) = OfNat.ofNat n
Full source 
@[simp, norm_cast] lemma ofENat_ofNat (n : ℕ) [n.AtLeastTwo] :
    ((ofNat(n) : ℕ∞) : Cardinal) = OfNat.ofNat n :=
  rfl
Embedding of Numerals ≥ 2 Preserves Cardinality: $\text{ofENat}(n) = n$ for $n \geq 2$
Informal description
For any natural number $n \geq 2$, the embedding of $n$ into extended natural numbers followed by the coercion to cardinal numbers equals the canonical embedding of $n$ as a cardinal number, i.e., $\text{ofENat}(n) = n$ where $n$ is interpreted in $\text{Cardinal}$.
Cardinal.ofENat_strictMono theorem
: StrictMono ofENat
Full source 
lemma ofENat_strictMono : StrictMono ofENat :=
  WithTop.strictMono_iff.2 ⟨Nat.strictMono_cast, nat_lt_aleph0⟩
Strict Monotonicity of the Extended Natural Number to Cardinal Embedding
Informal description
The function $\text{ofENat} : \mathbb{N}_\infty \to \text{Cardinal}$ is strictly monotone. That is, for any extended natural numbers $m, n \in \mathbb{N}_\infty$, if $m < n$ then $\text{ofENat}(m) < \text{ofENat}(n)$.
Cardinal.ofENat_lt_ofENat theorem
{m n : ℕ∞} : (m : Cardinal) < n ↔ m < n
Full source 
@[simp, norm_cast]
lemma ofENat_lt_ofENat {m n : ℕ∞} : (m : Cardinal) < n ↔ m < n :=
  ofENat_strictMono.lt_iff_lt
Order-Preserving Property of Extended Natural Number to Cardinal Embedding: $\text{ofENat}(m) < \text{ofENat}(n) \leftrightarrow m < n$
Informal description
For any extended natural numbers $m, n \in \mathbb{N}_\infty$, the cardinality corresponding to $m$ is strictly less than the cardinality corresponding to $n$ if and only if $m$ is strictly less than $n$ in the order on $\mathbb{N}_\infty$. In symbols: $\text{ofENat}(m) < \text{ofENat}(n) \leftrightarrow m < n$.
Cardinal.ofENat_lt_aleph0 theorem
{m : ℕ∞} : (m : Cardinal) < ℵ₀ ↔ m < ⊤
Full source 
@[simp, norm_cast]
lemma ofENat_lt_aleph0 {m : ℕ∞} : (m : Cardinal) < ℵ₀ ↔ m < ⊤ :=
  ofENat_lt_ofENat (n := ⊤)
Comparison of Extended Natural Number Cardinality with Aleph-null: $\text{ofENat}(m) < \aleph_0 \leftrightarrow m < \infty$
Informal description
For any extended natural number $m \in \mathbb{N}_\infty$, the cardinality corresponding to $m$ is strictly less than $\aleph_0$ if and only if $m$ is strictly less than $\infty$ (the top element of $\mathbb{N}_\infty$). In symbols: $\text{ofENat}(m) < \aleph_0 \leftrightarrow m < \infty$.
Cardinal.ofENat_lt_nat theorem
{m : ℕ∞} {n : ℕ} : ofENat m < n ↔ m < n
Full source 
@[simp] lemma ofENat_lt_nat {m : ℕ∞} {n : ℕ} : ofENatofENat m < n ↔ m < n := by norm_cast
Comparison of Extended Natural Number Cardinality with Natural Numbers: $\text{ofENat}(m) < n \leftrightarrow m < n$
Informal description
For any extended natural number $m \in \mathbb{N}_\infty$ and any natural number $n \in \mathbb{N}$, the cardinality corresponding to $m$ is strictly less than $n$ if and only if $m$ is strictly less than $n$ in the order on $\mathbb{N}_\infty$.
Cardinal.ofENat_lt_ofNat theorem
{m : ℕ∞} {n : ℕ} [n.AtLeastTwo] : ofENat m < ofNat(n) ↔ m < OfNat.ofNat n
Full source 
@[simp] lemma ofENat_lt_ofNat {m : ℕ∞} {n : ℕ} [n.AtLeastTwo] :
    ofENatofENat m < ofNat(n) ↔ m < OfNat.ofNat n := ofENat_lt_nat
Comparison of Extended Natural Number Cardinality with Numerals ≥ 2: $\text{ofENat}(m) < n \leftrightarrow m < n$
Informal description
For any extended natural number $m \in \mathbb{N}_\infty$ and any natural number $n \geq 2$, the cardinality corresponding to $m$ is strictly less than the cardinality corresponding to $n$ if and only if $m$ is strictly less than $n$ in the order on $\mathbb{N}_\infty$.
Cardinal.nat_lt_ofENat theorem
{m : ℕ} {n : ℕ∞} : (m : Cardinal) < n ↔ m < n
Full source 
@[simp] lemma nat_lt_ofENat {m : ℕ} {n : ℕ∞} : (m : Cardinal) < n ↔ m < n := by norm_cast
Comparison of Finite Cardinals with Extended Natural Numbers: $m < n$ iff $m < n$
Informal description
For any natural number $m$ and extended natural number $n$, the cardinality of $m$ is less than $n$ if and only if $m$ is less than $n$ in the extended natural numbers.
Cardinal.ofENat_pos theorem
{m : ℕ∞} : 0 < (m : Cardinal) ↔ 0 < m
Full source 
@[simp] lemma ofENat_pos {m : ℕ∞} : 0 < (m : Cardinal) ↔ 0 < m := by norm_cast
Positivity Preservation in Cardinal Embedding of Extended Naturals
Informal description
For any extended natural number $m \in \mathbb{N}_\infty$, the cardinal number obtained from $m$ is strictly positive if and only if $m$ is strictly positive. In other words, $0 < \text{ofENat}(m) \leftrightarrow 0 < m$.
Cardinal.one_lt_ofENat theorem
{m : ℕ∞} : 1 < (m : Cardinal) ↔ 1 < m
Full source 
@[simp] lemma one_lt_ofENat {m : ℕ∞} : 1 < (m : Cardinal) ↔ 1 < m := by norm_cast
Preservation of $1 < m$ between extended naturals and cardinals
Informal description
For any extended natural number $m \in \mathbb{N}_\infty$, the inequality $1 < m$ holds in the extended natural numbers if and only if the corresponding inequality $1 < m$ holds when $m$ is interpreted as a cardinal number via the embedding $\mathbb{N}_\infty \to \text{Cardinal}$.
Cardinal.ofNat_lt_ofENat theorem
{m : ℕ} [m.AtLeastTwo] {n : ℕ∞} : (ofNat(m) : Cardinal) < n ↔ OfNat.ofNat m < n
Full source 
@[simp, norm_cast] lemma ofNat_lt_ofENat {m : ℕ} [m.AtLeastTwo] {n : ℕ∞} :
  (ofNat(m) : Cardinal) < n ↔ OfNat.ofNat m < n := nat_lt_ofENat
Comparison of Finite Cardinals ≥2 with Extended Naturals: $m < n$ iff $m < n$
Informal description
For any natural number $m \geq 2$ and extended natural number $n \in \mathbb{N}_\infty$, the cardinality of $m$ is strictly less than $n$ if and only if $m$ is strictly less than $n$ in the extended natural numbers.
Cardinal.ofENat_mono theorem
: Monotone ofENat
Full source 
lemma ofENat_mono : Monotone ofENat := ofENat_strictMono.monotone
Monotonicity of the Extended Natural Number to Cardinal Embedding
Informal description
The function $\text{ofENat} : \mathbb{N}_\infty \to \text{Cardinal}$ is monotone. That is, for any extended natural numbers $m, n \in \mathbb{N}_\infty$, if $m \leq n$ then $\text{ofENat}(m) \leq \text{ofENat}(n)$.
Cardinal.ofENat_le_ofENat theorem
{m n : ℕ∞} : (m : Cardinal) ≤ n ↔ m ≤ n
Full source 
@[simp, norm_cast]
lemma ofENat_le_ofENat {m n : ℕ∞} : (m : Cardinal) ≤ n ↔ m ≤ n := ofENat_strictMono.le_iff_le
Comparison of Extended Natural Numbers via Cardinal Embedding: $\text{Cardinal.ofENat}(m) \leq \text{Cardinal.ofENat}(n) \leftrightarrow m \leq n$
Informal description
For any extended natural numbers $m, n \in \mathbb{N}_\infty$, the cardinality of $m$ is less than or equal to the cardinality of $n$ if and only if $m \leq n$ in the extended natural numbers. In symbols: \[ \text{Cardinal.ofENat}(m) \leq \text{Cardinal.ofENat}(n) \leftrightarrow m \leq n. \]
Cardinal.ofENat_le_aleph0 theorem
(n : ℕ∞) : ↑n ≤ ℵ₀
Full source 
@[simp] lemma ofENat_le_aleph0 (n : ℕ∞) : ↑n ≤ ℵ₀ := ofENat_le_ofENat.2 le_top
Cardinality of Extended Natural Numbers Bounded by Aleph-null
Informal description
For any extended natural number $n \in \mathbb{N}_\infty$, the cardinality of $n$ (via the embedding $\text{Cardinal.ofENat}$) is less than or equal to $\aleph_0$, the first infinite cardinal. In symbols: \[ \text{Cardinal.ofENat}(n) \leq \aleph_0. \]
Cardinal.ofENat_le_nat theorem
{m : ℕ∞} {n : ℕ} : ofENat m ≤ n ↔ m ≤ n
Full source 
@[simp] lemma ofENat_le_nat {m : ℕ∞} {n : ℕ} : ofENatofENat m ≤ n ↔ m ≤ n := by norm_cast
Comparison of Extended Natural Numbers and Cardinals: $\text{Cardinal.ofENat}(m) \leq n \leftrightarrow m \leq n$
Informal description
For any extended natural number $m \in \mathbb{N}_\infty$ and any natural number $n \in \mathbb{N}$, the cardinality of $m$ is less than or equal to $n$ if and only if $m$ is less than or equal to $n$ in the extended natural numbers. In symbols: \[ \text{Cardinal.ofENat}(m) \leq n \leftrightarrow m \leq n. \]
Cardinal.ofENat_le_one theorem
{m : ℕ∞} : ofENat m ≤ 1 ↔ m ≤ 1
Full source 
@[simp] lemma ofENat_le_one {m : ℕ∞} : ofENatofENat m ≤ 1 ↔ m ≤ 1 := by norm_cast
Cardinality of Extended Natural Number Bounded by One
Informal description
For any extended natural number $m \in \mathbb{N}_\infty$, the cardinality $\text{ofENat}(m)$ is less than or equal to 1 if and only if $m \leq 1$.
Cardinal.ofENat_le_ofNat theorem
{m : ℕ∞} {n : ℕ} [n.AtLeastTwo] : ofENat m ≤ ofNat(n) ↔ m ≤ OfNat.ofNat n
Full source 
@[simp] lemma ofENat_le_ofNat {m : ℕ∞} {n : ℕ} [n.AtLeastTwo] :
    ofENatofENat m ≤ ofNat(n) ↔ m ≤ OfNat.ofNat n := ofENat_le_nat
Comparison of Extended Natural Numbers and Cardinals for $n \geq 2$: $\text{Cardinal.ofENat}(m) \leq n \leftrightarrow m \leq n$
Informal description
For any extended natural number $m \in \mathbb{N}_\infty$ and any natural number $n \geq 2$, the inequality $\text{Cardinal.ofENat}(m) \leq n$ holds if and only if $m \leq n$ in $\mathbb{N}_\infty$.
Cardinal.nat_le_ofENat theorem
{m : ℕ} {n : ℕ∞} : (m : Cardinal) ≤ n ↔ m ≤ n
Full source 
@[simp] lemma nat_le_ofENat {m : ℕ} {n : ℕ∞} : (m : Cardinal) ≤ n ↔ m ≤ n := by norm_cast
Comparison of Natural Number Cardinality with Extended Natural Numbers: $(m : \text{Cardinal}) \leq n \leftrightarrow m \leq n$
Informal description
For any natural number $m$ and extended natural number $n$, the cardinality of $m$ is less than or equal to $n$ if and only if $m$ is less than or equal to $n$ in the extended natural numbers.
Cardinal.one_le_ofENat theorem
{n : ℕ∞} : 1 ≤ (n : Cardinal) ↔ 1 ≤ n
Full source 
@[simp] lemma one_le_ofENat {n : ℕ∞} : 1 ≤ (n : Cardinal) ↔ 1 ≤ n := by norm_cast
Comparison of One with Cardinal Image of Extended Natural Number
Informal description
For any extended natural number $n \in \mathbb{N}_\infty$, the cardinality $1$ is less than or equal to the cardinal image of $n$ if and only if $1 \leq n$ in $\mathbb{N}_\infty$.
Cardinal.ofNat_le_ofENat theorem
{m : ℕ} [m.AtLeastTwo] {n : ℕ∞} : (ofNat(m) : Cardinal) ≤ n ↔ OfNat.ofNat m ≤ n
Full source 
@[simp]
lemma ofNat_le_ofENat {m : ℕ} [m.AtLeastTwo] {n : ℕ∞} :
    (ofNat(m) : Cardinal) ≤ n ↔ OfNat.ofNat m ≤ n := nat_le_ofENat
Comparison of Cardinality for Numerals $\geq 2$: $(m : \text{Cardinal}) \leq n \leftrightarrow m \leq n$
Informal description
For any natural number $m \geq 2$ and extended natural number $n \in \mathbb{N}_\infty$, the cardinality of $m$ is less than or equal to $n$ if and only if $m \leq n$ in $\mathbb{N}_\infty$.
Cardinal.ofENat_injective theorem
: Injective ofENat
Full source 
lemma ofENat_injective : Injective ofENat := ofENat_strictMono.injective
Injectivity of the Extended Natural Number to Cardinal Embedding
Informal description
The function $\text{ofENat} : \mathbb{N}_\infty \to \text{Cardinal}$ is injective. That is, for any extended natural numbers $m, n \in \mathbb{N}_\infty$, if $\text{ofENat}(m) = \text{ofENat}(n)$, then $m = n$.
Cardinal.ofENat_inj theorem
{m n : ℕ∞} : (m : Cardinal) = n ↔ m = n
Full source 
@[simp, norm_cast]
lemma ofENat_inj {m n : ℕ∞} : (m : Cardinal) = n ↔ m = n := ofENat_injective.eq_iff
Equivalence of Cardinal and Extended Natural Number Equality: $(m : \text{Cardinal}) = n \leftrightarrow m = n$
Informal description
For any extended natural numbers $m, n \in \mathbb{N}_\infty$, the equality $(m : \text{Cardinal}) = n$ holds if and only if $m = n$ in $\mathbb{N}_\infty$.
Cardinal.ofENat_eq_nat theorem
{m : ℕ∞} {n : ℕ} : (m : Cardinal) = n ↔ m = n
Full source 
@[simp] lemma ofENat_eq_nat {m : ℕ∞} {n : ℕ} : (m : Cardinal) = n ↔ m = n := by norm_cast
Equality of Extended Natural Number and Natural Number as Cardinals: $(m : \text{Cardinal}) = n \leftrightarrow m = n$
Informal description
For any extended natural number $m \in \mathbb{N}_\infty$ and any natural number $n \in \mathbb{N}$, the cardinality of $m$ equals the cardinality of $n$ if and only if $m = n$.
Cardinal.nat_eq_ofENat theorem
{m : ℕ} {n : ℕ∞} : (m : Cardinal) = n ↔ m = n
Full source 
@[simp] lemma nat_eq_ofENat {m : ℕ} {n : ℕ∞} : (m : Cardinal) = n ↔ m = n := by norm_cast
Equality of Finite Cardinal and Extended Natural Number: $(m : \text{Cardinal}) = n \leftrightarrow m = n$
Informal description
For any natural number $m$ and extended natural number $n$, the cardinality of $m$ (as a cardinal number) equals the cardinality of $n$ if and only if $m = n$ as extended natural numbers.
Cardinal.ofENat_eq_zero theorem
{m : ℕ∞} : (m : Cardinal) = 0 ↔ m = 0
Full source 
@[simp] lemma ofENat_eq_zero {m : ℕ∞} : (m : Cardinal) = 0 ↔ m = 0 := by norm_cast
Embedding of Zero in Extended Natural Numbers to Cardinals
Informal description
For any extended natural number $m \in \mathbb{N}_\infty$, the cardinal number obtained by embedding $m$ equals the zero cardinal if and only if $m$ equals zero, i.e., $\text{Cardinal.ofENat}(m) = 0 \leftrightarrow m = 0$.
Cardinal.zero_eq_ofENat theorem
{m : ℕ∞} : 0 = (m : Cardinal) ↔ m = 0
Full source 
@[simp] lemma zero_eq_ofENat {m : ℕ∞} : 0 = (m : Cardinal) ↔ m = 0 := by norm_cast; apply eq_comm
Zero Cardinal Equals Embedding of Extended Natural Number if and only if Zero
Informal description
For any extended natural number $m \in \mathbb{N}_\infty$, the zero cardinal is equal to the cardinal embedding of $m$ if and only if $m$ is equal to zero, i.e., $0 = \text{Cardinal.ofENat}(m) \leftrightarrow m = 0$.
Cardinal.ofENat_eq_one theorem
{m : ℕ∞} : (m : Cardinal) = 1 ↔ m = 1
Full source 
@[simp] lemma ofENat_eq_one {m : ℕ∞} : (m : Cardinal) = 1 ↔ m = 1 := by norm_cast
Cardinality Embedding Preserves One: $(m : \text{Cardinal}) = 1 \leftrightarrow m = 1$
Informal description
For any extended natural number $m \in \mathbb{N}_\infty$, the cardinality embedding of $m$ equals the cardinal number $1$ if and only if $m$ equals $1$.
Cardinal.one_eq_ofENat theorem
{m : ℕ∞} : 1 = (m : Cardinal) ↔ m = 1
Full source 
@[simp] lemma one_eq_ofENat {m : ℕ∞} : 1 = (m : Cardinal) ↔ m = 1 := by norm_cast; apply eq_comm
Equivalence of One in Cardinals and Extended Naturals: $1 = \text{ofENat}(m) \leftrightarrow m = 1$
Informal description
For any extended natural number $m \in \mathbb{N}_\infty$, the cardinal number $1$ equals the image of $m$ under the embedding $\text{Cardinal.ofENat}$ if and only if $m$ equals the natural number $1$. In other words, $1 = \text{Cardinal.ofENat}(m) \leftrightarrow m = 1$.
Cardinal.ofENat_eq_ofNat theorem
{m : ℕ∞} {n : ℕ} [n.AtLeastTwo] : (m : Cardinal) = ofNat(n) ↔ m = OfNat.ofNat n
Full source 
@[simp] lemma ofENat_eq_ofNat {m : ℕ∞} {n : ℕ} [n.AtLeastTwo] :
    (m : Cardinal) = ofNat(n) ↔ m = OfNat.ofNat n := ofENat_eq_nat
Equality of Extended Natural Number and Natural Number ≥ 2 as Cardinals: $(m : \text{Cardinal}) = n \leftrightarrow m = n$
Informal description
For any extended natural number $m \in \mathbb{N}_\infty$ and any natural number $n \geq 2$, the cardinality of $m$ equals the cardinality of the natural number $n$ if and only if $m$ is equal to $n$ (viewed as an extended natural number via the canonical embedding).
Cardinal.ofNat_eq_ofENat theorem
{m : ℕ} {n : ℕ∞} [m.AtLeastTwo] : ofNat(m) = (n : Cardinal) ↔ OfNat.ofNat m = n
Full source 
@[simp] lemma ofNat_eq_ofENat {m : ℕ} {n : ℕ∞} [m.AtLeastTwo] :
    ofNat(m)ofNat(m) = (n : Cardinal) ↔ OfNat.ofNat m = n := nat_eq_ofENat
Equality of Numeral Cardinal and Extended Natural Embedding: $\text{ofNat}(m) = n \leftrightarrow m = n$ for $m \geq 2$
Informal description
For any natural number $m \geq 2$ and extended natural number $n$, the cardinal number represented by the numeral $m$ equals the cardinal image of $n$ under the embedding $\mathbb{N}_\infty \to \text{Cardinal}$ if and only if $m$ equals $n$ as extended natural numbers. In other words: $$ \text{ofNat}(m) = n \leftrightarrow m = n $$
Cardinal.lift_ofENat theorem
: ∀ m : ℕ∞, lift.{u, v} m = m
Full source 
@[simp, norm_cast] lemma lift_ofENat : ∀ m : ℕ∞, lift.{u, v} m = m
  | (m : ℕ) => lift_natCast m
  | ⊤ => lift_aleph0
Lift Invariance of Extended Natural Numbers in Cardinals
Informal description
For any extended natural number $m \in \mathbb{N}_\infty$, the lift operation applied to $m$ preserves its value as a cardinal number, i.e., $\text{lift}(m) = m$.
Cardinal.lift_lt_ofENat theorem
{x : Cardinal.{v}} {m : ℕ∞} : lift.{u} x < m ↔ x < m
Full source 
@[simp] lemma lift_lt_ofENat {x : CardinalCardinal.{v}} {m : ℕ∞} : liftlift.{u} x < m ↔ x < m := by
  rw [← lift_ofENat.{u, v}, lift_lt]
Lift Preserves Order Relation with Extended Natural Numbers
Informal description
For any cardinal number $x$ in universe `Type v` and any extended natural number $m \in \mathbb{N}_\infty$, the lifted cardinal $\text{lift}(x)$ is less than $m$ if and only if $x$ is less than $m$.
Cardinal.lift_eq_ofENat theorem
{x : Cardinal.{v}} {m : ℕ∞} : lift.{u} x = m ↔ x = m
Full source 
@[simp] lemma lift_eq_ofENat {x : CardinalCardinal.{v}} {m : ℕ∞} : liftlift.{u} x = m ↔ x = m := by
  rw [← lift_ofENat.{u, v}, lift_inj]
Lift Invariance of Equality between Cardinals and Extended Natural Numbers
Informal description
For any cardinal number $x$ in universe `Type v` and any extended natural number $m \in \mathbb{N}_\infty$, the lift of $x$ to universe `Type (max v u)` equals $m$ if and only if $x$ equals $m$.
Cardinal.ofENat_le_lift theorem
{x : Cardinal.{v}} {m : ℕ∞} : m ≤ lift.{u} x ↔ m ≤ x
Full source 
@[simp] lemma ofENat_le_lift {x : CardinalCardinal.{v}} {m : ℕ∞} : m ≤ lift.{u} x ↔ m ≤ x := by
  rw [← lift_ofENat.{u, v}, lift_le]
Comparison of Extended Natural Numbers with Lifted Cardinals: $m \leq \text{lift}(x) ↔ m \leq x$
Informal description
For any cardinal number $x$ in universe `Type v` and any extended natural number $m \in \mathbb{N}_\infty$, the inequality $m \leq \text{lift}(x)$ holds if and only if $m \leq x$ holds.
Cardinal.range_ofENat theorem
: range ofENat = Iic ℵ₀
Full source 
@[simp]
lemma range_ofENat : range ofENat = Iic ℵ₀ := by
  refine (range_subset_iff.2 ofENat_le_aleph0).antisymm fun x (hx : x ≤ ℵ₀) ↦ ?_
  rcases hx.lt_or_eq with hlt | rfl
  · lift x to ℕ using hlt
    exact mem_range_self (x : ℕ∞)
  · exact mem_range_self (⊤ : ℕ∞)
Range of Extended Natural Number Embedding in Cardinals is Bounded by $\aleph_0$
Informal description
The range of the embedding function $\text{Cardinal.ofENat} : \mathbb{N}_\infty \to \text{Cardinal}$ is equal to the set of all cardinal numbers less than or equal to $\aleph_0$. In other words, the image of $\mathbb{N}_\infty$ under this embedding is precisely the set $\{\kappa \in \text{Cardinal} \mid \kappa \leq \aleph_0\}$.
Cardinal.instCanLiftENatOfENatLeAleph0 instance
: CanLift Cardinal ℕ∞ (↑) (· ≤ ℵ₀)
Full source 
instance : CanLift Cardinal ℕ∞ (↑) (· ≤ ℵ₀) where
  prf x := (Set.ext_iff.1 range_ofENat x).2
Lifting Condition from Cardinals to Extended Naturals via $\aleph_0$-Bounded Embedding
Informal description
There exists a lifting condition from cardinal numbers to extended natural numbers via the canonical embedding function $\text{Cardinal.ofENat} : \mathbb{N}_\infty \to \text{Cardinal}$, where the condition for lifting is that the cardinal number is less than or equal to $\aleph_0$. This means that any cardinal $\kappa$ satisfying $\kappa \leq \aleph_0$ can be represented as an extended natural number under this embedding.
Cardinal.toENatAux definition
: Cardinal.{u} → ℕ∞
Full source 
/-- Unbundled version of `Cardinal.toENat`. -/
noncomputable def toENatAux : CardinalCardinal.{u} → ℕ∞ := extend Nat.cast Nat.cast fun _ ↦ ⊤
Auxiliary function from cardinals to extended natural numbers
Informal description
The auxiliary function `Cardinal.toENatAux` maps a cardinal number $\kappa$ to an extended natural number as follows: if $\kappa$ is the cardinality of a finite type (i.e., $\kappa = n$ for some natural number $n$), then it returns $n$; otherwise, it returns $\infty$. More precisely, this is defined by extending the canonical embedding of natural numbers into both cardinal numbers and extended natural numbers, mapping any infinite cardinal to $\infty$.
Cardinal.toENatAux_nat theorem
(n : ℕ) : toENatAux n = n
Full source 
lemma toENatAux_nat (n : ℕ) : toENatAux n = n := Nat.cast_injective.extend_apply ..
Auxiliary Cardinal-to-ENat Function Preserves Natural Numbers
Informal description
For any natural number $n$, the auxiliary function $\mathrm{toENatAux}$ maps $n$ to itself, i.e., $\mathrm{toENatAux}(n) = n$.
Cardinal.toENatAux_zero theorem
: toENatAux 0 = 0
Full source 
lemma toENatAux_zero : toENatAux 0 = 0 := toENatAux_nat 0
$\mathrm{toENatAux}(0) = 0$
Informal description
The auxiliary function $\mathrm{toENatAux}$ maps the zero cardinal to the zero element of the extended natural numbers, i.e., $\mathrm{toENatAux}(0) = 0$.
Cardinal.toENatAux_eq_top theorem
{a : Cardinal} (ha : ℵ₀ ≤ a) : toENatAux a = ⊤
Full source 
lemma toENatAux_eq_top {a : Cardinal} (ha : ℵ₀ ≤ a) : toENatAux a = ⊤ :=
  extend_apply' _ _ _ fun ⟨n, hn⟩ ↦ ha.not_lt <| hn ▸ nat_lt_aleph0 n
Mapping Infinite Cardinals to Infinity in Extended Naturals
Informal description
For any cardinal number $a$ such that $\aleph_0 \leq a$, the auxiliary function $\mathrm{toENatAux}$ maps $a$ to the infinity element $\top$ of the extended natural numbers $\mathbb{N}_\infty$.
Cardinal.toENatAux_ofENat theorem
: ∀ n : ℕ∞, toENatAux n = n
Full source 
lemma toENatAux_ofENat : ∀ n : ℕ∞, toENatAux n = n
  | (n : ℕ) => toENatAux_nat n
  | ⊤ => toENatAux_eq_top le_rfl
Auxiliary Cardinal-to-ENat Function is Identity on Extended Naturals
Informal description
For any extended natural number $n \in \mathbb{N}_\infty$, the auxiliary function $\mathrm{toENatAux}$ maps $n$ to itself, i.e., $\mathrm{toENatAux}(n) = n$.
Cardinal.toENatAux_gc theorem
: GaloisConnection (↑) toENatAux
Full source 
lemma toENatAux_gc : GaloisConnection (↑) toENatAux := fun n x ↦ by
  cases lt_or_le x ℵ₀ with
  | inl hx => lift x to ℕ using hx; simp
  | inr hx => simp [toENatAux_eq_top hx, (ofENat_le_aleph0 n).trans hx]
Galois Connection Between Cardinal Embedding and Auxiliary Projection
Informal description
The function `Cardinal.ofENat` (denoted by the coercion `↑`) and the auxiliary function `toENatAux` form a Galois connection between the extended natural numbers $\mathbb{N}_\infty$ and the cardinal numbers. That is, for any $n \in \mathbb{N}_\infty$ and any cardinal $\kappa$, we have: \[ \uparrow n \leq \kappa \quad \text{if and only if} \quad n \leq \mathrm{toENatAux}(\kappa). \]
Cardinal.toENatAux_le_nat theorem
{x : Cardinal} {n : ℕ} : toENatAux x ≤ n ↔ x ≤ n
Full source 
theorem toENatAux_le_nat {x : Cardinal} {n : ℕ} : toENatAuxtoENatAux x ≤ n ↔ x ≤ n := by
  cases lt_or_le x ℵ₀ with
  | inl hx => lift x to ℕ using hx; simp
  | inr hx => simp [toENatAux_eq_top hx, (nat_lt_aleph0 n).trans_le hx]
Comparison of Cardinal-to-ENat Auxiliary Function with Natural Numbers: $\mathrm{toENatAux}(x) \leq n \leftrightarrow x \leq n$
Informal description
For any cardinal number $x$ and natural number $n$, the auxiliary function $\mathrm{toENatAux}(x)$ is less than or equal to $n$ if and only if $x$ is less than or equal to $n$ as cardinal numbers.
Cardinal.toENatAux_eq_nat theorem
{x : Cardinal} {n : ℕ} : toENatAux x = n ↔ x = n
Full source 
lemma toENatAux_eq_nat {x : Cardinal} {n : ℕ} : toENatAuxtoENatAux x = n ↔ x = n := by
  simp only [le_antisymm_iff, toENatAux_le_nat, ← toENatAux_gc _, ofENat_nat]
Cardinal-to-ENat Auxiliary Function Equals Natural Number iff Cardinal Equals Natural Number
Informal description
For any cardinal number $x$ and natural number $n$, the auxiliary function $\mathrm{toENatAux}(x)$ equals $n$ if and only if $x$ equals $n$ as a cardinal number.
Cardinal.toENatAux_eq_zero theorem
{x : Cardinal} : toENatAux x = 0 ↔ x = 0
Full source 
lemma toENatAux_eq_zero {x : Cardinal} : toENatAuxtoENatAux x = 0 ↔ x = 0 := toENatAux_eq_nat
$\mathrm{toENatAux}(x) = 0 \leftrightarrow x = 0$ for cardinals
Informal description
For any cardinal number $x$, the auxiliary function $\mathrm{toENatAux}(x)$ equals $0$ if and only if $x$ equals $0$ as a cardinal number.
Cardinal.toENat definition
: Cardinal.{u} →+*o ℕ∞
Full source 
/-- Projection from cardinals to `ℕ∞`. Sends all infinite cardinals to `⊤`.

We define this function as a bundled monotone ring homomorphism. -/
noncomputable def toENat : CardinalCardinal.{u}Cardinal.{u} →+*o ℕ∞ where
  toFun := toENatAux
  map_one' := toENatAux_nat 1
  map_mul' x y := by
    wlog hle : x ≤ y; · rw [mul_comm, this y x (le_of_not_le hle), mul_comm]
    cases lt_or_le y ℵ₀ with
    | inl hy =>
      lift x to ℕ using hle.trans_lt hy; lift y to ℕ using hy
      simp only [← Nat.cast_mul, toENatAux_nat]
    | inr hy =>
      rcases eq_or_ne x 0 with rfl | hx
      · simp
      · simp only [toENatAux_eq_top hy]
        rw [toENatAux_eq_top, ENat.mul_top]
        · rwa [Ne, toENatAux_eq_zero]
        · exact le_mul_of_one_le_of_le (one_le_iff_ne_zero.2 hx) hy
  map_add' x y := by
    wlog hle : x ≤ y; · rw [add_comm, this y x (le_of_not_le hle), add_comm]
    cases lt_or_le y ℵ₀ with
    | inl hy =>
      lift x to ℕ using hle.trans_lt hy; lift y to ℕ using hy
      simp only [← Nat.cast_add, toENatAux_nat]
    | inr hy =>
      simp only [toENatAux_eq_top hy, add_top]
      exact toENatAux_eq_top <| le_add_left hy
  map_zero' := toENatAux_zero
  monotone' := toENatAux_gc.monotone_u
Projection from cardinals to extended natural numbers
Informal description
The function $\mathrm{toENat}$ maps a cardinal number $\kappa$ to an extended natural number as follows: if $\kappa$ is finite (i.e., $\kappa = n$ for some natural number $n$), then it returns $n$; otherwise, it returns $\infty$. This function is a monotone ring homomorphism, preserving addition, multiplication, and the order relation.
Cardinal.enat_gc theorem
: GaloisConnection (↑) toENat
Full source 
/-- The coercion `Cardinal.ofENat` and the projection `Cardinal.toENat` form a Galois connection.
See also `Cardinal.gciENat`. -/
lemma enat_gc : GaloisConnection (↑) toENat := toENatAux_gc
Galois Connection Between Extended Naturals and Cardinals
Informal description
The coercion function $\mathrm{ofENat} : \mathbb{N}_\infty \to \mathrm{Cardinal}$ and the projection function $\mathrm{toENat} : \mathrm{Cardinal} \to \mathbb{N}_\infty$ form a Galois connection. That is, for any extended natural number $n \in \mathbb{N}_\infty$ and any cardinal number $\kappa$, we have: \[ \mathrm{ofENat}(n) \leq \kappa \quad \text{if and only if} \quad n \leq \mathrm{toENat}(\kappa). \]
Cardinal.toENat_ofENat theorem
(n : ℕ∞) : toENat n = n
Full source 
@[simp] lemma toENat_ofENat (n : ℕ∞) : toENat n = n := toENatAux_ofENat n
Projection of Extended Naturals is Identity
Informal description
For any extended natural number $n \in \mathbb{N}_\infty$, the projection from cardinals to extended natural numbers satisfies $\mathrm{toENat}(n) = n$.
Cardinal.toENat_comp_ofENat theorem
: toENat ∘ (↑) = id
Full source 
@[simp] lemma toENat_comp_ofENat : toENattoENat ∘ (↑) = id := funext toENat_ofENat
Composition of Projection and Embedding Yields Identity on Extended Naturals
Informal description
The composition of the projection from cardinals to extended natural numbers with the embedding of extended natural numbers into cardinals is equal to the identity function on $\mathbb{N}_\infty$, i.e., $\mathrm{toENat} \circ \mathrm{ofENat} = \mathrm{id}$.
Cardinal.gciENat definition
: GaloisCoinsertion (↑) toENat
Full source 
/-- The coercion `Cardinal.ofENat` and the projection `Cardinal.toENat`
form a Galois coinsertion. -/
noncomputable def gciENat : GaloisCoinsertion (↑) toENat :=
  enat_gc.toGaloisCoinsertion fun n ↦ (toENat_ofENat n).le
Galois coinsertion between extended naturals and cardinals
Informal description
The coercion function $\mathrm{ofENat} : \mathbb{N}_\infty \to \mathrm{Cardinal}$ and the projection function $\mathrm{toENat} : \mathrm{Cardinal} \to \mathbb{N}_\infty$ form a Galois coinsertion. That is, they satisfy the following properties: 1. For any extended natural number $n \in \mathbb{N}_\infty$, we have $\mathrm{toENat}(\mathrm{ofENat}(n)) = n$. 2. The functions form a Galois connection, meaning that for any $n \in \mathbb{N}_\infty$ and cardinal $\kappa$, we have $\mathrm{ofENat}(n) \leq \kappa$ if and only if $n \leq \mathrm{toENat}(\kappa)$.
Cardinal.toENat_strictMonoOn theorem
: StrictMonoOn toENat (Iic ℵ₀)
Full source 
lemma toENat_strictMonoOn : StrictMonoOn toENat (Iic ℵ₀) := by
  simp only [← range_ofENat, StrictMonoOn, forall_mem_range, toENat_ofENat, ofENat_lt_ofENat]
  exact fun _ _ ↦ id
Strict Monotonicity of Cardinal-to-ENat Projection Below $\aleph_0$
Informal description
The function $\mathrm{toENat} : \mathrm{Cardinal} \to \mathbb{N}_\infty$ is strictly increasing on the set of cardinals less than or equal to $\aleph_0$. That is, for any two cardinals $\kappa, \lambda \leq \aleph_0$, if $\kappa < \lambda$ then $\mathrm{toENat}(\kappa) < \mathrm{toENat}(\lambda)$.
Cardinal.toENat_injOn theorem
: InjOn toENat (Iic ℵ₀)
Full source 
lemma toENat_injOn : InjOn toENat (Iic ℵ₀) := toENat_strictMonoOn.injOn
Injectivity of Cardinal-to-ENat Projection Below $\aleph_0$
Informal description
The projection function $\mathrm{toENat} : \mathrm{Cardinal} \to \mathbb{N}_\infty$ is injective when restricted to the set of cardinals less than or equal to $\aleph_0$. That is, for any two cardinals $\kappa, \lambda \leq \aleph_0$, if $\mathrm{toENat}(\kappa) = \mathrm{toENat}(\lambda)$, then $\kappa = \lambda$.
Cardinal.ofENat_toENat_le theorem
(a : Cardinal) : ↑(toENat a) ≤ a
Full source 
lemma ofENat_toENat_le (a : Cardinal) : ↑(toENat a) ≤ a := enat_gc.l_u_le _
Inequality for Cardinal Projection and Coercion: $\mathrm{ofENat}(\mathrm{toENat}(a)) \leq a$
Informal description
For any cardinal number $a$, the cardinality obtained by coercing its projection to extended natural numbers back to cardinals is less than or equal to $a$ itself, i.e., $\mathrm{ofENat}(\mathrm{toENat}(a)) \leq a$.
Cardinal.ofENat_toENat_eq_self theorem
{a : Cardinal} : toENat a = a ↔ a ≤ ℵ₀
Full source 
@[simp]
lemma ofENat_toENat_eq_self {a : Cardinal} : toENattoENat a = a ↔ a ≤ ℵ₀ := by
  rw [eq_comm, ← enat_gc.exists_eq_l]
  simpa only [mem_range, eq_comm] using Set.ext_iff.1 range_ofENat a
Characterization of Cardinals Fixed by $\mathrm{toENat}$ as Those Bounded by $\aleph_0$
Informal description
For any cardinal number $a$, the composition of the embedding $\mathrm{ofENat}$ and the projection $\mathrm{toENat}$ satisfies $\mathrm{toENat}(a) = a$ if and only if $a$ is less than or equal to $\aleph_0$.
Cardinal.toENat_nat theorem
(n : ℕ) : toENat n = n
Full source 
lemma toENat_nat (n : ℕ) : toENat n = n := map_natCast _ n
Projection of Natural Numbers to Extended Naturals Preserves Value
Informal description
For any natural number $n$, the projection of $n$ as a cardinal number to the extended natural numbers $\mathbb{N}_\infty$ equals $n$ itself, i.e., $\mathrm{toENat}(n) = n$.
Cardinal.toENat_le_nat theorem
{a : Cardinal} {n : ℕ} : toENat a ≤ n ↔ a ≤ n
Full source 
@[simp] lemma toENat_le_nat {a : Cardinal} {n : ℕ} : toENattoENat a ≤ n ↔ a ≤ n := toENatAux_le_nat
Comparison of Cardinal-to-ENat with Natural Numbers: $\mathrm{toENat}(a) \leq n \leftrightarrow a \leq n$
Informal description
For any cardinal number $a$ and natural number $n$, the extended natural number $\mathrm{toENat}(a)$ is less than or equal to $n$ if and only if $a \leq n$ as cardinal numbers.
Cardinal.toENat_eq_nat theorem
{a : Cardinal} {n : ℕ} : toENat a = n ↔ a = n
Full source 
@[simp] lemma toENat_eq_nat {a : Cardinal} {n : ℕ} : toENattoENat a = n ↔ a = n := toENatAux_eq_nat
Equivalence of Cardinal-to-ENat Projection and Natural Number Equality: $\mathrm{toENat}(a) = n \leftrightarrow a = n$
Informal description
For any cardinal number $a$ and natural number $n$, the projection $\mathrm{toENat}(a)$ equals $n$ if and only if $a$ equals $n$ as a cardinal number.
Cardinal.toENat_eq_zero theorem
{a : Cardinal} : toENat a = 0 ↔ a = 0
Full source 
@[simp] lemma toENat_eq_zero {a : Cardinal} : toENattoENat a = 0 ↔ a = 0 := toENatAux_eq_zero
$\mathrm{toENat}(a) = 0 \leftrightarrow a = 0$ for cardinals
Informal description
For any cardinal number $a$, the projection $\mathrm{toENat}(a)$ equals $0$ if and only if $a = 0$ as a cardinal number.
Cardinal.toENat_le_one theorem
{a : Cardinal} : toENat a ≤ 1 ↔ a ≤ 1
Full source 
@[simp] lemma toENat_le_one {a : Cardinal} : toENattoENat a ≤ 1 ↔ a ≤ 1 := toENat_le_nat
Comparison of Cardinal-to-ENat with One: $\mathrm{toENat}(a) \leq 1 \leftrightarrow a \leq 1$
Informal description
For any cardinal number $a$, the extended natural number $\mathrm{toENat}(a)$ is less than or equal to $1$ if and only if $a \leq 1$ as cardinal numbers.
Cardinal.toENat_eq_one theorem
{a : Cardinal} : toENat a = 1 ↔ a = 1
Full source 
@[simp] lemma toENat_eq_one {a : Cardinal} : toENattoENat a = 1 ↔ a = 1 := toENat_eq_nat
Equivalence of Cardinal-to-ENat Projection and One: $\mathrm{toENat}(a) = 1 \leftrightarrow a = 1$
Informal description
For any cardinal number $a$, the projection $\mathrm{toENat}(a)$ equals $1$ if and only if $a = 1$ as cardinal numbers.
Cardinal.toENat_le_ofNat theorem
{a : Cardinal} {n : ℕ} [n.AtLeastTwo] : toENat a ≤ ofNat(n) ↔ a ≤ OfNat.ofNat n
Full source 
@[simp] lemma toENat_le_ofNat {a : Cardinal} {n : ℕ} [n.AtLeastTwo] :
    toENattoENat a ≤ ofNat(n) ↔ a ≤ OfNat.ofNat n := toENat_le_nat
Comparison of Cardinal-to-ENat with Numerals ≥ 2: $\mathrm{toENat}(a) \leq n \leftrightarrow a \leq n$
Informal description
For any cardinal number $a$ and natural number $n \geq 2$, the extended natural number $\mathrm{toENat}(a)$ is less than or equal to $n$ if and only if $a \leq n$ as cardinal numbers.
Cardinal.toENat_eq_ofNat theorem
{a : Cardinal} {n : ℕ} [n.AtLeastTwo] : toENat a = ofNat(n) ↔ a = OfNat.ofNat n
Full source 
@[simp] lemma toENat_eq_ofNat {a : Cardinal} {n : ℕ} [n.AtLeastTwo] :
    toENattoENat a = ofNat(n) ↔ a = OfNat.ofNat n := toENat_eq_nat
Equivalence of Cardinal-to-ENat Projection and Numerals ≥ 2: $\mathrm{toENat}(a) = n \leftrightarrow a = n$
Informal description
For any cardinal number $a$ and natural number $n \geq 2$, the projection $\mathrm{toENat}(a)$ equals $n$ if and only if $a$ equals $n$ as a cardinal number.
Cardinal.toENat_eq_top theorem
{a : Cardinal} : toENat a = ⊤ ↔ ℵ₀ ≤ a
Full source 
@[simp] lemma toENat_eq_top {a : Cardinal} : toENattoENat a = ⊤ ↔ ℵ₀ ≤ a := enat_gc.u_eq_top
Projection to Extended Naturals Equals Infinity iff Aleph-null Bounds Cardinal
Informal description
For any cardinal number $a$, the projection to extended natural numbers satisfies $\mathrm{toENat}(a) = \infty$ if and only if $\aleph_0 \leq a$.
Cardinal.toENat_ne_top theorem
{a : Cardinal} : toENat a ≠ ⊤ ↔ a < ℵ₀
Full source 
lemma toENat_ne_top {a : Cardinal} : toENattoENat a ≠ ⊤toENat a ≠ ⊤ ↔ a < ℵ₀ := by simp
Finite Cardinals via $\mathrm{toENat}$ Projection: $\mathrm{toENat}(a) \neq \infty \leftrightarrow a < \aleph_0$
Informal description
For any cardinal number $a$, the projection $\mathrm{toENat}(a)$ is not equal to $\infty$ if and only if $a$ is strictly less than $\aleph_0$ (i.e., $a$ is a finite cardinal).
Cardinal.toENat_lt_top theorem
{a : Cardinal} : toENat a < ⊤ ↔ a < ℵ₀
Full source 
@[simp] lemma toENat_lt_top {a : Cardinal} : toENattoENat a < ⊤ ↔ a < ℵ₀ := by simp [lt_top_iff_ne_top]
Finite Cardinals Project to Finite Extended Naturals
Informal description
For any cardinal number $a$, the projection $\mathrm{toENat}(a)$ is strictly less than $\infty$ if and only if $a$ is strictly less than $\aleph_0$.
Cardinal.toENat_lift theorem
{a : Cardinal.{v}} : toENat (lift.{u} a) = toENat a
Full source 
@[simp]
theorem toENat_lift {a : CardinalCardinal.{v}} : toENat (lift.{u} a) = toENat a := by
  cases le_total a ℵ₀ with
  | inl ha => lift a to ℕ∞ using ha; simp
  | inr ha => simp [toENat_eq_top.2, ha]
Universe Lift Invariance of Cardinal Projection to Extended Naturals
Informal description
For any cardinal number $a$, the projection to extended natural numbers satisfies $\mathrm{toENat}(\mathrm{lift}(a)) = \mathrm{toENat}(a)$, where $\mathrm{lift}$ is the universe lift operation on cardinals.
Cardinal.toENat_congr theorem
{α : Type u} {β : Type v} (e : α ≃ β) : toENat #α = toENat #β
Full source 
theorem toENat_congr {α : Type u} {β : Type v} (e : α ≃ β) : toENat #α = toENat #β := by
  rw [← toENat_lift, lift_mk_eq.{_, _,v}.mpr ⟨e⟩, toENat_lift]
Bijection Preserves Cardinal Projection to Extended Naturals
Informal description
For any types $\alpha$ and $\beta$ with a bijection $e : \alpha \simeq \beta$, the extended natural number projections of their cardinalities are equal, i.e., $\mathrm{toENat}(\#\alpha) = \mathrm{toENat}(\#\beta)$.
Cardinal.toENat_le_iff_of_le_aleph0 theorem
{c c' : Cardinal} (h : c ≤ ℵ₀) : toENat c ≤ toENat c' ↔ c ≤ c'
Full source 
lemma toENat_le_iff_of_le_aleph0 {c c' : Cardinal} (h : c ≤ ℵ₀) :
    toENattoENat c ≤ toENat c' ↔ c ≤ c' := by
  lift c to ℕ∞ using h
  simp_rw [toENat_ofENat, enat_gc _]
Comparison of Cardinals via Extended Naturals for $\aleph_0$-Bounded Cardinals
Informal description
For any two cardinal numbers $c$ and $c'$ with $c \leq \aleph_0$, the inequality $\mathrm{toENat}(c) \leq \mathrm{toENat}(c')$ holds if and only if $c \leq c'$.
Cardinal.toENat_le_iff_of_lt_aleph0 theorem
{c c' : Cardinal} (hc' : c' < ℵ₀) : toENat c ≤ toENat c' ↔ c ≤ c'
Full source 
lemma toENat_le_iff_of_lt_aleph0 {c c' : Cardinal} (hc' : c' < ℵ₀) :
    toENattoENat c ≤ toENat c' ↔ c ≤ c' := by
  lift c' to ℕ using hc'
  simp_rw [toENat_nat, ← toENat_le_nat]
Comparison of Cardinals via Extended Naturals for Finite Cardinals
Informal description
For any two cardinal numbers $c$ and $c'$ with $c' < \aleph_0$, the inequality $\mathrm{toENat}(c) \leq \mathrm{toENat}(c')$ holds if and only if $c \leq c'$.
Cardinal.toENat_eq_iff_of_le_aleph0 theorem
{c c' : Cardinal} (hc : c ≤ ℵ₀) (hc' : c' ≤ ℵ₀) : toENat c = toENat c' ↔ c = c'
Full source 
lemma toENat_eq_iff_of_le_aleph0 {c c' : Cardinal} (hc : c ≤ ℵ₀) (hc' : c' ≤ ℵ₀) :
    toENattoENat c = toENat c' ↔ c = c' :=
  toENat_strictMonoOn.injOn.eq_iff hc hc'
Equality of Cardinals via Extended Naturals Below $\aleph_0$
Informal description
For any two cardinal numbers $c$ and $c'$ such that $c \leq \aleph_0$ and $c' \leq \aleph_0$, the equality $\mathrm{toENat}(c) = \mathrm{toENat}(c')$ holds if and only if $c = c'$.
Cardinal.ofENat_add theorem
(m n : ℕ∞) : ofENat (m + n) = m + n
Full source 
@[simp, norm_cast]
lemma ofENat_add (m n : ℕ∞) : ofENat (m + n) = m + n := by apply toENat_injOn <;> simp
Additivity of the Embedding $\mathbb{N}_\infty \to \text{Cardinal}$
Informal description
For any two extended natural numbers $m, n \in \mathbb{N}_\infty$, the embedding of their sum into cardinal numbers equals the sum of their embeddings, i.e., $\mathrm{ofENat}(m + n) = \mathrm{ofENat}(m) + \mathrm{ofENat}(n)$.
Cardinal.aleph0_add_ofENat theorem
(m : ℕ∞) : ℵ₀ + m = ℵ₀
Full source 
@[simp] lemma aleph0_add_ofENat (m : ℕ∞) : ℵ₀ + m = ℵ₀ := (ofENat_add ⊤ m).symm
$\aleph_0 + m = \aleph_0$ for any extended natural $m$
Informal description
For any extended natural number $m \in \mathbb{N}_\infty$, the sum of the first infinite cardinal $\aleph_0$ and the cardinal corresponding to $m$ equals $\aleph_0$, i.e., $\aleph_0 + m = \aleph_0$.
Cardinal.ofENat_add_aleph0 theorem
(m : ℕ∞) : m + ℵ₀ = ℵ₀
Full source 
@[simp] lemma ofENat_add_aleph0 (m : ℕ∞) : m + ℵ₀ = ℵ₀ := by rw [add_comm, aleph0_add_ofENat]
Sum of Extended Natural Cardinal and Aleph-Null is Aleph-Null
Informal description
For any extended natural number $m \in \mathbb{N}_\infty$, the sum of the cardinal number corresponding to $m$ and the first infinite cardinal $\aleph_0$ equals $\aleph_0$, i.e., $m + \aleph_0 = \aleph_0$.
Cardinal.ofENat_mul_aleph0 theorem
{m : ℕ∞} (hm : m ≠ 0) : ↑m * ℵ₀ = ℵ₀
Full source 
@[simp] lemma ofENat_mul_aleph0 {m : ℕ∞} (hm : m ≠ 0) : ↑m * ℵ₀ = ℵ₀ := by
  induction m with
  | top => exact aleph0_mul_aleph0
  | coe m => rw [ofENat_nat, nat_mul_aleph0 (mod_cast hm)]
Product of Extended Natural Cardinal and Aleph-Null is Aleph-Null
Informal description
For any extended natural number $m \in \mathbb{N}_\infty$ such that $m \neq 0$, the product of the cardinal number corresponding to $m$ and the first infinite cardinal $\aleph_0$ equals $\aleph_0$, i.e., $m \cdot \aleph_0 = \aleph_0$.
Cardinal.aleph0_mul_ofENat theorem
{m : ℕ∞} (hm : m ≠ 0) : ℵ₀ * m = ℵ₀
Full source 
@[simp] lemma aleph0_mul_ofENat {m : ℕ∞} (hm : m ≠ 0) : ℵ₀ * m = ℵ₀ := by
  rw [mul_comm, ofENat_mul_aleph0 hm]
$\aleph_0 \cdot m = \aleph_0$ for nonzero extended natural $m$
Informal description
For any extended natural number $m \in \mathbb{N}_\infty$ such that $m \neq 0$, the product of the first infinite cardinal $\aleph_0$ and the cardinal number corresponding to $m$ equals $\aleph_0$, i.e., $\aleph_0 \cdot m = \aleph_0$.
Cardinal.ofENat_mul theorem
(m n : ℕ∞) : ofENat (m * n) = m * n
Full source 
@[simp] lemma ofENat_mul (m n : ℕ∞) : ofENat (m * n) = m * n :=
  toENat_injOn (by simp)
    (aleph0_mul_aleph0 ▸ mul_le_mul' (ofENat_le_aleph0 _) (ofENat_le_aleph0 _)) (by simp)
Embedding Preserves Multiplication of Extended Natural Numbers in Cardinals
Informal description
For any extended natural numbers $m, n \in \mathbb{N}_\infty$, the embedding of their product into cardinal numbers equals the product of their embeddings, i.e., \[ \text{Cardinal.ofENat}(m * n) = \text{Cardinal.ofENat}(m) * \text{Cardinal.ofENat}(n). \]
Cardinal.ofENatHom definition
: ℕ∞ →+*o Cardinal
Full source 
/-- The coercion `Cardinal.ofENat` as a bundled homomorphism. -/
def ofENatHom : ℕ∞ℕ∞ →+*o Cardinal where
  toFun := (↑)
  map_one' := ofENat_one
  map_mul' := ofENat_mul
  map_zero' := ofENat_zero
  map_add' := ofENat_add
  monotone' := ofENat_mono
Extended natural numbers to cardinals homomorphism
Informal description
The bundled homomorphism version of the coercion `Cardinal.ofENat`, which maps an extended natural number $n \in \mathbb{N}_\infty$ to a cardinal number. This homomorphism preserves addition, multiplication, zero, one, and is monotone with respect to the natural orders on $\mathbb{N}_\infty$ and `Cardinal`.