mathlib3 documentation

set_theory.ordinal.principal

Principal ordinals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions and results #

Todo #

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
theorem ordinal.principal.iterate_lt {op : ordinal ordinal ordinal} {a o : ordinal} (hao : a < o) (ho : ordinal.principal op o) (n : ) :
op a^[n] a < o
theorem ordinal.op_eq_self_of_principal {op : ordinal ordinal ordinal} {a o : ordinal} (hao : a < o) (H : ordinal.is_normal (op a)) (ho : ordinal.principal op o) (ho' : o.is_limit) :
op a o = o
theorem ordinal.nfp_le_of_principal {op : ordinal ordinal ordinal} {a o : ordinal} (hao : a < o) (ho : ordinal.principal op o) :
ordinal.nfp (op a) a o

Principal ordinals are unbounded #

theorem ordinal.principal_nfp_blsub₂ (op : ordinal ordinal ordinal) (o : ordinal) :
ordinal.principal op (ordinal.nfp (λ (o' : ordinal), o'.blsub₂ o' (λ (a : ordinal) (_x : a < o') (b : ordinal) (_x : b < o'), op a b)) o)

Additive principal ordinals #

theorem ordinal.exists_lt_add_of_not_principal_add {a : ordinal} (ha : ¬ordinal.principal has_add.add a) :
(b c : ordinal) (hb : b < a) (hc : c < a), b + c = a

The main characterization theorem for additive principal ordinals.

theorem ordinal.add_absorp {a b c : ordinal} (h₁ : a < ordinal.omega ^ b) (h₂ : ordinal.omega ^ b c) :
a + c = c

Multiplicative principal ordinals #

theorem ordinal.mul_omega {a : ordinal} (a0 : 0 < a) (ha : a < ordinal.omega) :
theorem ordinal.mul_lt_omega_opow {a b c : ordinal} (c0 : 0 < c) (ha : a < ordinal.omega ^ c) (hb : b < ordinal.omega) :

The main characterization theorem for multiplicative principal ordinals.

theorem ordinal.mul_omega_dvd {a : ordinal} (a0 : 0 < a) (ha : a < ordinal.omega) {b : ordinal} :
theorem ordinal.mul_eq_opow_log_succ {a b : ordinal} (ha : a 0) (hb : ordinal.principal has_mul.mul b) (hb₂ : 2 < b) :
a * b = b ^ order.succ (ordinal.log b a)

Exponential principal ordinals #