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)
:
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)
:
@[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)
:
Alias of Cardinal.mk_iUnion_Ordinal_le_of_le
.
Cardinality of ordinals #
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})
:
theorem
Ordinal.card_opow_le_of_omega0_le_left
{a : Ordinal.{u_1}}
(ha : omega0 ≤ a)
(b : Ordinal.{u_1})
:
theorem
Ordinal.card_opow_le_of_omega0_le_right
(a : Ordinal.{u_1})
{b : Ordinal.{u_1}}
(hb : omega0 ≤ b)
:
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)
@[deprecated Ordinal.principal_add_omega (since := "2024-11-08")]
theorem
Cardinal.principal_add_aleph
(o : Ordinal.{u_1})
:
Ordinal.Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) (aleph o).ord