# Principal ordinals #

We define principal or indecomposable ordinals, and we prove the standard properties about them.

## Main definitions and results #

• Principal: A principal or indecomposable ordinal under some binary operation. We include 0 and any other typically excluded edge cases for simplicity.
• unbounded_principal: Principal ordinals are unbounded.
• principal_add_iff_zero_or_omega_opow: The main characterization theorem for additive principal ordinals.
• principal_mul_iff_le_two_or_omega_opow_opow: The main characterization theorem for multiplicative principal ordinals.

## TODO #

• Prove that exponential principal ordinals are 0, 1, 2, ω, or epsilon numbers, i.e. fixed points of fun x ↦ ω ^ x.

### Principal ordinals #

An ordinal o is said to be principal or indecomposable under an operation when the set of ordinals less than it is closed under that operation. In standard mathematical usage, this term is almost exclusively used for additive and multiplicative principal ordinals.

For simplicity, we break usual convention and regard 0 as principal.

Equations
Instances For
@[simp]
theorem Ordinal.principal_one_iff {op : } :
op 0 0 = 0
theorem Ordinal.Principal.iterate_lt {op : } {a : Ordinal.{u_1}} {o : Ordinal.{u_1}} (hao : a < o) (ho : ) (n : ) :
(op a)^[n] a < o
theorem Ordinal.op_eq_self_of_principal {op : } {a : Ordinal.{u}} {o : Ordinal.{u}} (hao : a < o) (H : Ordinal.IsNormal (op a)) (ho : ) (ho' : o.IsLimit) :
op a o = o
theorem Ordinal.nfp_le_of_principal {op : } {a : Ordinal.{u_1}} {o : Ordinal.{u_1}} (hao : a < o) (ho : ) :
Ordinal.nfp (op a) a o

### Principal ordinals are unbounded #

theorem Ordinal.principal_nfp_blsub₂ (op : ) (o : Ordinal.{u}) :
Ordinal.Principal op (Ordinal.nfp (fun (o' : Ordinal.{u}) => o'.blsub₂ o' fun (a : Ordinal.{u}) (x : a < o') (b : Ordinal.{u}) (x : b < o') => op a b) o)
theorem Ordinal.unbounded_principal (op : ) :
Set.Unbounded (fun (x x_1 : Ordinal.{u_1}) => x < x_1) {o : Ordinal.{u_1} | }

theorem Ordinal.principal_add_of_le_one {o : Ordinal.{u_1}} (ho : o 1) :
Ordinal.Principal (fun (x x_1 : Ordinal.{u_1}) => x + x_1) o
theorem Ordinal.principal_add_isLimit {o : Ordinal.{u_1}} (ho₁ : 1 < o) (ho : Ordinal.Principal (fun (x x_1 : Ordinal.{u_1}) => x + x_1) o) :
o.IsLimit
Ordinal.Principal (fun (x x_1 : Ordinal.{u_1}) => x + x_1) o a < o, a + o = o
theorem Ordinal.exists_lt_add_of_not_principal_add {a : Ordinal.{u_1}} (ha : ¬Ordinal.Principal (fun (x x_1 : Ordinal.{u_1}) => x + x_1) a) :
∃ (b : Ordinal.{u_1}) (c : Ordinal.{u_1}), b < a c < a b + c = a
Ordinal.Principal (fun (x x_1 : Ordinal.{u_1}) => x + x_1) a ∀ ⦃b c : Ordinal.{u_1}⦄, b < ac < ab + c a
theorem Ordinal.add_omega {a : Ordinal.{u_1}} (h : ) :
theorem Ordinal.add_omega_opow {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (h : a < ) :
a + =

The main characterization theorem for additive principal ordinals.

theorem Ordinal.opow_principal_add_of_principal_add {a : Ordinal.{u_1}} (ha : Ordinal.Principal (fun (x x_1 : Ordinal.{u_1}) => x + x_1) a) (b : Ordinal.{u_1}) :
Ordinal.Principal (fun (x x_1 : Ordinal.{u_1}) => x + x_1) (a ^ b)
theorem Ordinal.add_absorp {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (h₁ : a < ) (h₂ : c) :
a + c = c
theorem Ordinal.mul_principal_add_is_principal_add (a : Ordinal.{u}) {b : Ordinal.{u}} (hb₁ : b 1) (hb : Ordinal.Principal (fun (x x_1 : Ordinal.{u}) => x + x_1) b) :
Ordinal.Principal (fun (x x_1 : Ordinal.{u}) => x + x_1) (a * b)

#### Multiplicative principal ordinals #

theorem Ordinal.principal_mul_of_le_two {o : Ordinal.{u_1}} (ho : o 2) :
Ordinal.Principal (fun (x x_1 : Ordinal.{u_1}) => x * x_1) o
theorem Ordinal.principal_add_of_principal_mul {o : Ordinal.{u_1}} (ho : Ordinal.Principal (fun (x x_1 : Ordinal.{u_1}) => x * x_1) o) (ho₂ : o 2) :
Ordinal.Principal (fun (x x_1 : Ordinal.{u_1}) => x + x_1) o
theorem Ordinal.principal_mul_isLimit {o : Ordinal.{u}} (ho₂ : 2 < o) (ho : Ordinal.Principal (fun (x x_1 : Ordinal.{u}) => x * x_1) o) :
o.IsLimit
theorem Ordinal.principal_mul_iff_mul_left_eq {o : Ordinal.{u_1}} :
Ordinal.Principal (fun (x x_1 : Ordinal.{u_1}) => x * x_1) o ∀ (a : Ordinal.{u_1}), 0 < aa < oa * o = o
theorem Ordinal.mul_omega {a : Ordinal.{u_1}} (a0 : 0 < a) (ha : ) :
theorem Ordinal.mul_lt_omega_opow {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (c0 : 0 < c) (ha : a < ) (hb : ) :
a * b <
theorem Ordinal.mul_omega_opow_opow {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (a0 : 0 < a) (h : ) :
theorem Ordinal.principal_add_of_principal_mul_opow {o : Ordinal.{u_1}} {b : Ordinal.{u_1}} (hb : 1 < b) (ho : Ordinal.Principal (fun (x x_1 : Ordinal.{u_1}) => x * x_1) (b ^ o)) :
Ordinal.Principal (fun (x x_1 : Ordinal.{u_1}) => x + x_1) o

The main characterization theorem for multiplicative principal ordinals.

theorem Ordinal.mul_omega_dvd {a : Ordinal.{u_1}} (a0 : 0 < a) (ha : ) {b : Ordinal.{u_1}} :
a * b = b
theorem Ordinal.mul_eq_opow_log_succ {a : Ordinal.{u}} {b : Ordinal.{u}} (ha : a 0) (hb : Ordinal.Principal (fun (x x_1 : Ordinal.{u}) => x * x_1) b) (hb₂ : 2 < b) :
a * b = b ^ Order.succ ()

#### Exponential principal ordinals #

theorem Ordinal.opow_omega {a : Ordinal.{u_1}} (a1 : 1 < a) (h : ) :