Ordinal arithmetic with cardinals

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

Cardinal operations with ordinal indices

theorem Cardinal.mk_biUnion_le_of_le_lift {β : 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.

@[deprecated Cardinal.mk_biUnion_le_of_le_lift (since := "2026-01-26")]

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

Alias of Cardinal.mk_biUnion_le_of_le_lift.

---

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

theorem Cardinal.mk_biUnion_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_biUnion_le_of_le (since := "2026-01-26")]

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

Alias of Cardinal.mk_biUnion_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 i.toOrd).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_le_of_omega0_le_left {a : Ordinal.{u_1}} (ha : omega0 ≤ a) (b : Ordinal.{u_1}) : (a ^ b).card ≤ max a.card b.card

theorem Ordinal.card_opow_le_of_omega0_le_right (a : Ordinal.{u_1}) {b : Ordinal.{u_1}} (hb : omega0 ≤ b) : (a ^ b).card ≤ max a.card b.card

theorem Ordinal.card_opow_le (a b : Ordinal.{u_1}) : (a ^ b).card ≤ max Cardinal.aleph0 (max a.card b.card)

theorem Ordinal.card_opow_eq_of_omega0_le_left {a b : Ordinal.{u_1}} (ha : omega0 ≤ a) (hb : 0 < b) : (a ^ b).card = max 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 = max a.card b.card

theorem Ordinal.card_omega0_opow {a : Ordinal.{u_1}} (h : a ≠ 0) : (omega0 ^ a).card = max Cardinal.aleph0 a.card

theorem Ordinal.card_opow_omega0 {a : Ordinal.{u_1}} (h : 1 < a) : (a ^ omega0).card = max Cardinal.aleph0 a.card

theorem Ordinal.principal_opow_omega (o : Ordinal.{u_1}) : Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 ^ x2) (omega o)

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

theorem Ordinal.principal_opow_ord {c : Cardinal.{u_1}} (hc : Cardinal.aleph0 ≤ c) : Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 ^ x2) c.ord

Initial ordinals are principal

theorem Ordinal.principal_add_ord {c : Cardinal.{u_1}} (hc : Cardinal.aleph0 ≤ c) : Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) c.ord

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.principal_add_omega (o : Ordinal.{u_1}) : Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) (omega o)

theorem Ordinal.principal_mul_ord {c : Cardinal.{u_1}} (hc : Cardinal.aleph0 ≤ c) : Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 * x2) c.ord

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

theorem Ordinal.principal_mul_omega (o : Ordinal.{u_1}) : Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 * x2) (omega o)