Documentation

Mathlib.SetTheory.Ordinal.CantorNormalForm

Cantor Normal Form #

The Cantor normal form of an ordinal is generally defined as its base ω expansion, with its non-zero exponents in decreasing order. Here, we more generally define a base b expansion Ordinal.CNF in this manner, which is well-behaved for any b ≥ 2.

Implementation notes #

We implement Ordinal.CNF as an association list, where keys are exponents and values are coefficients. This is because this structure intrinsically reflects two key properties of the Cantor normal form:

It is ordered.
It has finitely many entries.

Todo #

Prove the basic results relating the CNF to the arithmetic operations on ordinals.

Cantor normal form as a list #

@[irreducible]

def Ordinal.CNF.rec (b : Ordinal.{u_2}) {C : Ordinal.{u_2} → Sort u_1} (H0 : C 0) (H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o) (o : Ordinal.{u_2}) :

C o

Inducts on the base b expansion of an ordinal.

Equations

Ordinal.CNF.rec b H0 H o = if h : o = 0 then ⋯ ▸ H0 else H o h (Ordinal.CNF.rec b H0 H (o % b ^ Ordinal.log b o))

Instances For

@[deprecated Ordinal.CNF.rec (since := "2025-08-18")]

def Ordinal.CNFRec (b : Ordinal.{u_2}) {C : Ordinal.{u_2} → Sort u_1} (H0 : C 0) (H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o) (o : Ordinal.{u_2}) :

C o

Alias of Ordinal.CNF.rec.

Inducts on the base b expansion of an ordinal.

Equations

Ordinal.CNFRec = Ordinal.CNF.rec

Instances For

@[simp]

theorem Ordinal.CNF.rec_zero {C : Ordinal.{u_2} → Sort u_1} (b : Ordinal.{u_2}) (H0 : C 0) (H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o) :

CNF.rec b H0 H 0 = H0

@[deprecated Ordinal.CNF.rec_zero (since := "2025-08-18")]

theorem Ordinal.CNFRec_zero {C : Ordinal.{u_2} → Sort u_1} (b : Ordinal.{u_2}) (H0 : C 0) (H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o) :

CNF.rec b H0 H 0 = H0

Alias of Ordinal.CNF.rec_zero.

theorem Ordinal.CNF.rec_pos (b : Ordinal.{u_2}) {o : Ordinal.{u_2}} {C : Ordinal.{u_2} → Sort u_1} (ho : o ≠ 0) (H0 : C 0) (H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o) :

CNF.rec b H0 H o = H o ho (CNF.rec b H0 H (o % b ^ log b o))

@[deprecated Ordinal.CNF.rec_pos (since := "2025-08-18")]

theorem Ordinal.CNFRec_pos (b : Ordinal.{u_2}) {o : Ordinal.{u_2}} {C : Ordinal.{u_2} → Sort u_1} (ho : o ≠ 0) (H0 : C 0) (H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o) :

CNF.rec b H0 H o = H o ho (CNF.rec b H0 H (o % b ^ log b o))

Alias of Ordinal.CNF.rec_pos.

def Ordinal.CNF (b o : Ordinal.{u_1}) :

List (Ordinal.{u_1} × Ordinal.{u_1})

The Cantor normal form of an ordinal o is the list of coefficients and exponents in the base-b expansion of o.

We special-case CNF 0 o = CNF 1 o = [(0, o)] for o ≠ 0.

CNF b (b ^ u₁ * v₁ + b ^ u₂ * v₂) = [(u₁, v₁), (u₂, v₂)]

Equations

Ordinal.CNF b o = Ordinal.CNF.rec b [] (fun (o : Ordinal.{?u.14}) (x : o ≠ 0) (IH : List (Ordinal.{?u.14} × Ordinal.{?u.14})) => (Ordinal.log b o, o / b ^ Ordinal.log b o) :: IH) o

Instances For

@[simp]

theorem Ordinal.CNF.zero_right (b : Ordinal.{u_1}) :

CNF b 0 = []

@[deprecated Ordinal.CNF.zero_right (since := "2025-08-18")]

theorem Ordinal.CNF_zero (b : Ordinal.{u_1}) :

CNF b 0 = []

Alias of Ordinal.CNF.zero_right.

theorem Ordinal.CNF.ne_zero {b o : Ordinal.{u_1}} (ho : o ≠ 0) :

CNF b o = (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)

Recursive definition for the Cantor normal form.

@[deprecated Ordinal.CNF.ne_zero (since := "2025-08-18")]

theorem Ordinal.CNF_ne_zero {b o : Ordinal.{u_1}} (ho : o ≠ 0) :

CNF b o = (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)

Alias of Ordinal.CNF.ne_zero.

Recursive definition for the Cantor normal form.

theorem Ordinal.CNF.zero_left {o : Ordinal.{u_1}} (ho : o ≠ 0) :

CNF 0 o = [(0, o)]

@[deprecated Ordinal.CNF.zero_left (since := "2025-08-18")]

theorem Ordinal.zero_CNF {o : Ordinal.{u_1}} (ho : o ≠ 0) :

CNF 0 o = [(0, o)]

Alias of Ordinal.CNF.zero_left.

theorem Ordinal.CNF.one_left {o : Ordinal.{u_1}} (ho : o ≠ 0) :

CNF 1 o = [(0, o)]

@[deprecated Ordinal.CNF.one_left (since := "2025-08-18")]

theorem Ordinal.one_CNF {o : Ordinal.{u_1}} (ho : o ≠ 0) :

CNF 1 o = [(0, o)]

Alias of Ordinal.CNF.one_left.

theorem Ordinal.CNF.of_le_one {b o : Ordinal.{u_1}} (hb : b ≤ 1) (ho : o ≠ 0) :

CNF b o = [(0, o)]

@[deprecated Ordinal.CNF.of_le_one (since := "2025-08-18")]

theorem Ordinal.CNF_of_le_one {b o : Ordinal.{u_1}} (hb : b ≤ 1) (ho : o ≠ 0) :

CNF b o = [(0, o)]

Alias of Ordinal.CNF.of_le_one.

theorem Ordinal.CNF.of_lt {b o : Ordinal.{u_1}} (ho : o ≠ 0) (hb : o < b) :

CNF b o = [(0, o)]

@[deprecated Ordinal.CNF.of_lt (since := "2025-08-18")]

theorem Ordinal.CNF_of_lt {b o : Ordinal.{u_1}} (ho : o ≠ 0) (hb : o < b) :

CNF b o = [(0, o)]

Alias of Ordinal.CNF.of_lt.

theorem Ordinal.CNF.foldr (b o : Ordinal.{u_1}) :

List.foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) => b ^ p.1 * p.2 + r) 0 (CNF b o) = o

Evaluating the Cantor normal form of an ordinal returns the ordinal.

@[deprecated Ordinal.CNF.foldr (since := "2025-08-18")]

theorem Ordinal.CNF_foldr (b o : Ordinal.{u_1}) :

List.foldr (fun (p : Ordinal.{u_1} × Ordinal.{u_1}) (r : Ordinal.{u_1}) => b ^ p.1 * p.2 + r) 0 (CNF b o) = o

Alias of Ordinal.CNF.foldr.

Evaluating the Cantor normal form of an ordinal returns the ordinal.

theorem Ordinal.CNF.fst_le_log {b o : Ordinal.{u}} {x : Ordinal.{u} × Ordinal.{u}} :

x ∈ CNF b o → x.1 ≤ log b o

Every exponent in the Cantor normal form CNF b o is less or equal to log b o.

@[deprecated Ordinal.CNF.fst_le_log (since := "2025-08-18")]

theorem Ordinal.CNF_fst_le_log {b o : Ordinal.{u}} {x : Ordinal.{u} × Ordinal.{u}} :

x ∈ CNF b o → x.1 ≤ log b o

Alias of Ordinal.CNF.fst_le_log.

Every exponent in the Cantor normal form CNF b o is less or equal to log b o.

theorem Ordinal.CNF.lt_snd {b o : Ordinal.{u}} {x : Ordinal.{u} × Ordinal.{u}} :

x ∈ CNF b o → 0 < x.2

Every coefficient in a Cantor normal form is positive.

@[deprecated Ordinal.CNF.lt_snd (since := "2025-08-18")]

theorem Ordinal.CNF_lt_snd {b o : Ordinal.{u}} {x : Ordinal.{u} × Ordinal.{u}} :

x ∈ CNF b o → 0 < x.2

Alias of Ordinal.CNF.lt_snd.

Every coefficient in a Cantor normal form is positive.

theorem Ordinal.CNF.snd_lt {b o : Ordinal.{u}} (hb : 1 < b) {x : Ordinal.{u} × Ordinal.{u}} :

x ∈ CNF b o → x.2 < b

Every coefficient in the Cantor normal form CNF b o is less than b.

@[deprecated Ordinal.CNF.snd_lt (since := "2025-08-18")]

theorem Ordinal.CNF_snd_lt {b o : Ordinal.{u}} (hb : 1 < b) {x : Ordinal.{u} × Ordinal.{u}} :

x ∈ CNF b o → x.2 < b

Alias of Ordinal.CNF.snd_lt.

Every coefficient in the Cantor normal form CNF b o is less than b.

theorem Ordinal.CNF.sorted (b o : Ordinal.{u_1}) :

List.Sorted (fun (x1 x2 : Ordinal.{u_1}) => x1 > x2) (List.map Prod.fst (CNF b o))

The exponents of the Cantor normal form are decreasing.

@[deprecated Ordinal.CNF.sorted (since := "2025-08-18")]

theorem Ordinal.CNF_sorted (b o : Ordinal.{u_1}) :

List.Sorted (fun (x1 x2 : Ordinal.{u_1}) => x1 > x2) (List.map Prod.fst (CNF b o))

Alias of Ordinal.CNF.sorted.

The exponents of the Cantor normal form are decreasing.

Cantor normal form as a finsupp #

def Ordinal.CNF.coeff (b o : Ordinal.{u_1}) :

Ordinal.{u_1} →₀ Ordinal.{u_1}

CNF.coeff b o is the finitely supported function returning the coefficient of b ^ e in the Cantor Normal Form (CNF) of o, for each e.

Equations

Ordinal.CNF.coeff b o = { entries := List.map Prod.toSigma (Ordinal.CNF b o), nodupKeys := ⋯ }.lookupFinsupp

Instances For

theorem Ordinal.CNF.coeff_of_mem_CNF {b o e c : Ordinal.{u_1}} (h : (e, c) ∈ CNF b o) :

(coeff b o) e = c

theorem Ordinal.CNF.coeff_of_not_mem_CNF {b o e : Ordinal.{u_1}} (h : e ∉ List.map Prod.fst (CNF b o)) :

(coeff b o) e = 0

theorem Ordinal.CNF.coeff_zero_apply (b e : Ordinal.{u_1}) :

(coeff b 0) e = 0

@[simp]

theorem Ordinal.CNF.coeff_zero_right (b : Ordinal.{u_1}) :

coeff b 0 = 0

theorem Ordinal.CNF.coeff_of_le_one {b : Ordinal.{u_1}} (hb : b ≤ 1) (o : Ordinal.{u_1}) :

coeff b o = Finsupp.single 0 o

@[simp]

theorem Ordinal.CNF.coeff_zero_left (o : Ordinal.{u_1}) :

coeff 0 o = Finsupp.single 0 o

@[simp]

theorem Ordinal.CNF.coeff_one_left (o : Ordinal.{u_1}) :

coeff 1 o = Finsupp.single 0 o