Documentation

Mathlib.SetTheory.Ordinal.Principal

Principal ordinals #

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
Instances For
    theorem Ordinal.not_principal_iff {op : Ordinal.{u_1}Ordinal.{u_1}Ordinal.{u_1}} {o : Ordinal.{u_1}} :
    ¬Ordinal.Principal op o a < o, b < o, o op a b
    theorem Ordinal.principal_iff_of_monotone {op : Ordinal.{u_1}Ordinal.{u_1}Ordinal.{u_1}} {o : Ordinal.{u_1}} (h₁ : ∀ (a : Ordinal.{u_1}), Monotone (op a)) (h₂ : ∀ (a : Ordinal.{u_1}), Monotone (Function.swap op a)) :
    Ordinal.Principal op o a < o, op a a < o
    theorem Ordinal.Principal.iterate_lt {op : Ordinal.{u_1}Ordinal.{u_1}Ordinal.{u_1}} {a : Ordinal.{u_1}} {o : Ordinal.{u_1}} (hao : a < o) (ho : Ordinal.Principal op o) (n : ) :
    (op a)^[n] a < o
    theorem Ordinal.op_eq_self_of_principal {op : Ordinal.{u}Ordinal.{u}Ordinal.{u}} {a : Ordinal.{u}} {o : Ordinal.{u}} (hao : a < o) (H : Ordinal.IsNormal (op a)) (ho : Ordinal.Principal op o) (ho' : o.IsLimit) :
    op a o = o

    Principal ordinals are unbounded #

    Principal ordinals under any operation are unbounded.

    @[deprecated]
    theorem Ordinal.principal_nfp_blsub₂ (op : Ordinal.{u}Ordinal.{u}Ordinal.{u}) (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)

    Additive principal ordinals #

    theorem Ordinal.principal_add_of_le_one {o : Ordinal.{u_1}} (ho : o 1) :
    Ordinal.Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) o
    theorem Ordinal.principal_add_isLimit {o : Ordinal.{u_1}} (ho₁ : 1 < o) (ho : Ordinal.Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) o) :
    o.IsLimit
    theorem Ordinal.principal_add_iff_add_left_eq_self {o : Ordinal.{u_1}} :
    Ordinal.Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) o a < o, a + o = o
    theorem Ordinal.exists_lt_add_of_not_principal_add {a : Ordinal.{u_1}} (ha : ¬Ordinal.Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) a) :
    b < a, c < a, b + c = a
    theorem Ordinal.principal_add_iff_add_lt_ne_self {a : Ordinal.{u_1}} :
    Ordinal.Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) a b < a, c < a, b + c a
    @[deprecated Ordinal.add_omega0]

    Alias of Ordinal.add_omega0.

    @[deprecated Ordinal.principal_add_omega0]

    Alias of Ordinal.principal_add_omega0.

    @[deprecated Ordinal.add_omega0_opow]

    Alias of Ordinal.add_omega0_opow.

    @[deprecated Ordinal.principal_add_omega0_opow]

    Alias of Ordinal.principal_add_omega0_opow.

    The main characterization theorem for additive principal ordinals.

    @[deprecated Ordinal.principal_add_iff_zero_or_omega0_opow]

    Alias of Ordinal.principal_add_iff_zero_or_omega0_opow.


    The main characterization theorem for additive principal ordinals.

    theorem Ordinal.opow_principal_add_of_principal_add {a : Ordinal.{u_1}} (ha : Ordinal.Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) a) (b : Ordinal.{u_1}) :
    Ordinal.Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) (a ^ b)
    theorem Ordinal.add_absorp {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (h₁ : a < Ordinal.omega0 ^ b) (h₂ : Ordinal.omega0 ^ b 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 (x1 x2 : Ordinal.{u}) => x1 + x2) b) :
    Ordinal.Principal (fun (x1 x2 : Ordinal.{u}) => x1 + x2) (a * b)

    Multiplicative principal ordinals #

    theorem Ordinal.principal_mul_of_le_two {o : Ordinal.{u_1}} (ho : o 2) :
    Ordinal.Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 * x2) o
    theorem Ordinal.principal_add_of_principal_mul {o : Ordinal.{u_1}} (ho : Ordinal.Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 * x2) o) (ho₂ : o 2) :
    Ordinal.Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) o
    theorem Ordinal.principal_mul_isLimit {o : Ordinal.{u}} (ho₂ : 2 < o) (ho : Ordinal.Principal (fun (x1 x2 : Ordinal.{u}) => x1 * x2) o) :
    o.IsLimit
    theorem Ordinal.principal_mul_iff_mul_left_eq {o : Ordinal.{u_1}} :
    Ordinal.Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 * x2) o ∀ (a : Ordinal.{u_1}), 0 < aa < oa * o = o
    @[deprecated Ordinal.principal_mul_omega0]

    Alias of Ordinal.principal_mul_omega0.

    @[deprecated Ordinal.mul_omega0]

    Alias of Ordinal.mul_omega0.

    @[deprecated Ordinal.mul_lt_omega0_opow]
    theorem Ordinal.mul_lt_omega_opow {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (c0 : 0 < c) (ha : a < Ordinal.omega0 ^ c) (hb : b < Ordinal.omega0) :

    Alias of Ordinal.mul_lt_omega0_opow.

    @[deprecated Ordinal.principal_mul_omega0_opow_opow]

    Alias of Ordinal.principal_mul_omega0_opow_opow.

    theorem Ordinal.principal_add_of_principal_mul_opow {o : Ordinal.{u_1}} {b : Ordinal.{u_1}} (hb : 1 < b) (ho : Ordinal.Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 * x2) (b ^ o)) :
    Ordinal.Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) o

    The main characterization theorem for multiplicative principal ordinals.

    @[deprecated Ordinal.principal_mul_iff_le_two_or_omega0_opow_opow]

    Alias of Ordinal.principal_mul_iff_le_two_or_omega0_opow_opow.


    The main characterization theorem for multiplicative principal ordinals.

    theorem Ordinal.mul_omega0_dvd {a : Ordinal.{u_1}} (a0 : 0 < a) (ha : a < Ordinal.omega0) {b : Ordinal.{u_1}} :
    Ordinal.omega0 ba * b = b
    @[deprecated Ordinal.mul_omega0_dvd]
    theorem Ordinal.mul_omega_dvd {a : Ordinal.{u_1}} (a0 : 0 < a) (ha : a < Ordinal.omega0) {b : Ordinal.{u_1}} :
    Ordinal.omega0 ba * b = b

    Alias of Ordinal.mul_omega0_dvd.

    theorem Ordinal.mul_eq_opow_log_succ {a : Ordinal.{u}} {b : Ordinal.{u}} (ha : a 0) (hb : Ordinal.Principal (fun (x1 x2 : Ordinal.{u}) => x1 * x2) b) (hb₂ : 2 < b) :
    a * b = b ^ Order.succ (Ordinal.log b a)

    Exponential principal ordinals #

    @[deprecated Ordinal.principal_opow_omega0]

    Alias of Ordinal.principal_opow_omega0.

    @[deprecated Ordinal.opow_omega0]

    Alias of Ordinal.opow_omega0.