Documentation

Mathlib.SetTheory.Cardinal.Ordinal

Ordinal arithmetic with cardinals #

This file collects results about the cardinality of different ordinal operations.

Cardinal operations with ordinal indices #

theorem Cardinal.mk_iUnion_Ordinal_lift_le_of_le {β : Type v} {o : Ordinal.{u}} {c : Cardinal.{v}} (ho : lift.{v, u} o.card lift.{u, v} c) (hc : aleph0 c) (A : Ordinal.{u}Set β) (hA : j < o, mk (A j) c) :
mk (⋃ (j : Ordinal.{u}), ⋃ (_ : j < o), A j) c

Bounds the cardinal of an ordinal-indexed union of sets.

theorem Cardinal.mk_iUnion_Ordinal_le_of_le {β : Type u_1} {o : Ordinal.{u_1}} {c : Cardinal.{u_1}} (ho : o.card c) (hc : aleph0 c) (A : Ordinal.{u_1}Set β) (hA : j < o, mk (A j) c) :
mk (⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < o), A j) c
@[deprecated Cardinal.mk_iUnion_Ordinal_le_of_le (since := "2024-11-02")]
theorem Ordinal.Cardinal.mk_iUnion_Ordinal_le_of_le {β : Type u_1} {o : Ordinal.{u_1}} {c : Cardinal.{u_1}} (ho : o.card c) (hc : Cardinal.aleph0 c) (A : Ordinal.{u_1}Set β) (hA : j < o, Cardinal.mk (A j) c) :
Cardinal.mk (⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < o), A j) c

Alias of Cardinal.mk_iUnion_Ordinal_le_of_le.

Cardinality of ordinals #

theorem Ordinal.lift_card_iSup_le_sum_card {ι : Type u} [Small.{v, u} ι] (f : ιOrdinal.{v}) :
Cardinal.lift.{u, v} (⨆ (i : ι), f i).card Cardinal.sum fun (i : ι) => (f i).card
theorem Ordinal.card_iSup_le_sum_card {ι : Type u} (f : ιOrdinal.{max u v}) :
(⨆ (i : ι), f i).card Cardinal.sum fun (i : ι) => (f i).card
theorem Ordinal.card_iSup_Iio_le_sum_card {o : Ordinal.{u}} (f : (Set.Iio o)Ordinal.{max u v}) :
(⨆ (a : (Set.Iio o)), f a).card Cardinal.sum fun (i : o.toType) => (f (o.enumIsoToType.symm i)).card
theorem Ordinal.card_iSup_Iio_le_card_mul_iSup {o : Ordinal.{u}} (f : (Set.Iio o)Ordinal.{max u v}) :
(⨆ (a : (Set.Iio o)), f a).card Cardinal.lift.{v, u} o.card * ⨆ (a : (Set.Iio o)), (f a).card
theorem Ordinal.card_opow_eq_of_omega0_le_left {a b : Ordinal.{u_1}} (ha : omega0 a) (hb : 0 < b) :
(a ^ b).card = a.card b.card
theorem Ordinal.card_opow_eq_of_omega0_le_right {a b : Ordinal.{u_1}} (ha : 1 < a) (hb : omega0 b) :
(a ^ b).card = a.card b.card
theorem Ordinal.IsInitial.principal_opow {o : Ordinal.{u_1}} (h : o.IsInitial) (ho : omega0 o) :
Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 ^ x2) o

Initial ordinals are principal #

theorem Ordinal.IsInitial.principal_add {o : Ordinal.{u_1}} (h : o.IsInitial) (ho : omega0 o) :
Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) o
theorem Ordinal.IsInitial.principal_mul {o : Ordinal.{u_1}} (h : o.IsInitial) (ho : omega0 o) :
Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 * x2) o
@[deprecated Ordinal.principal_add_omega (since := "2024-11-08")]