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.

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

Cardinality of ordinals

theorem Ordinal.lift_card_iSup_le_sum_card {ι : Type 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_iSup_le_lift {ι : Type u} {c : Cardinal.{v}} {f : ι → Ordinal.{v}} (hι : Cardinal.lift.{v, u} (Cardinal.mk ι) ≤ Cardinal.lift.{u, v} c) (hf : ∀ (i : ι), (f i).card ≤ c) : (⨆ (i : ι), f i).card ≤ c

theorem Ordinal.card_iSup_le {ι : Type u_1} {c : Cardinal.{u_1}} {f : ι → Ordinal.{u_1}} (hι : Cardinal.mk ι ≤ c) (hf : ∀ (i : ι), (f i).card ≤ c) : (⨆ (i : ι), f i).card ≤ c

theorem Ordinal.card_iSup_Iio_le_of_lift {o : Ordinal.{u}} {c : Cardinal.{v}} {f : ↑(Set.Iio o) → Ordinal.{v}} (hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c) (hf : ∀ (i : ↑(Set.Iio o)), (f i).card ≤ c) : (⨆ (i : ↑(Set.Iio o)), f i).card ≤ c

theorem Ordinal.card_iSup_Iio_le {o : Ordinal.{u_1}} {c : Cardinal.{u_1}} {f : ↑(Set.Iio o) → Ordinal.{u_1}} (hι : o.card ≤ c) (hf : ∀ (i : ↑(Set.Iio o)), (f i).card ≤ c) : (⨆ (i : ↑(Set.Iio o)), f i).card ≤ c

theorem Ordinal.card_sSup_le {c : Cardinal.{u}} {s : Set Ordinal.{u}} (hs : Cardinal.mk ↑s ≤ Cardinal.lift.{u + 1, u} c) (hs' : ∀ x ∈ s, x.card ≤ c) : (sSup s).card ≤ c

theorem Ordinal.card_nfpFamily_le {ι : Type v} {f : ι → Ordinal.{u} → Ordinal.{u}} {c : Cardinal.{u}} (hc : Cardinal.aleph0 ≤ c) (hι : Cardinal.lift.{u, v} (Cardinal.mk ι) ≤ Cardinal.lift.{v, u} c) (hf : ∀ (i : ι) (x : Ordinal.{u}), (f i x).card ≤ max c x.card) (o : Ordinal.{u}) : (nfpFamily f o).card ≤ max c o.card

theorem Ordinal.card_derivFamily_le {ι : Type v} {f : ι → Ordinal.{u} → Ordinal.{u}} {c : Cardinal.{u}} (hc : Cardinal.aleph0 ≤ c) (hι : Cardinal.lift.{u, v} (Cardinal.mk ι) ≤ Cardinal.lift.{v, u} c) (hf : ∀ (i : ι) (x : Ordinal.{u}), (f i x).card ≤ max c x.card) (o : Ordinal.{u}) : (derivFamily f o).card ≤ max c o.card

theorem Ordinal.card_nfp_le_of_forall_le {o : Ordinal.{u_1}} {f : Ordinal.{u_1} → Ordinal.{u_1}} (hf : ∀ (x : Ordinal.{u_1}), (f x).card ≤ max Cardinal.aleph0 x.card) : (nfp f o).card ≤ max Cardinal.aleph0 o.card

theorem Ordinal.card_deriv_le_of_forall_le {o : Ordinal.{u_1}} {f : Ordinal.{u_1} → Ordinal.{u_1}} (hf : ∀ (x : Ordinal.{u_1}), (f x).card ≤ max Cardinal.aleph0 x.card) : (deriv f o).card ≤ max Cardinal.aleph0 o.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.isPrincipal_opow_omega (o : Ordinal.{u_1}) : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 ^ x2) (omega o)

theorem Ordinal.IsInitial.isPrincipal_opow {o : Ordinal.{u_1}} (h : o.IsInitial) (ho : omega0 ≤ o) : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 ^ x2) o

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

Initial ordinals are principal

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

theorem Ordinal.IsInitial.isPrincipal_add {o : Ordinal.{u_1}} (h : o.IsInitial) (ho : omega0 ≤ o) : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) o

theorem Ordinal.isPrincipal_add_omega (o : Ordinal.{u_1}) : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) (omega o)

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

theorem Ordinal.IsInitial.isPrincipal_mul {o : Ordinal.{u_1}} (h : o.IsInitial) (ho : omega0 ≤ o) : IsPrincipal (fun (x1 x2 : Ordinal.{u_1}) => x1 * x2) o

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