# Cardinals and ordinals #

Relationships between cardinals and ordinals, properties of cardinals that are proved using ordinals.

## Main definitions #

• The function Cardinal.aleph' gives the cardinals listed by their ordinal index, and is the inverse of Cardinal.aleph/idx. aleph' n = n, aleph' ω = ℵ₀, aleph' (ω + 1) = succ ℵ₀, etc. It is an order isomorphism between ordinals and cardinals.
• The function Cardinal.aleph gives the infinite cardinals listed by their ordinal index. aleph 0 = ℵ₀, aleph 1 = succ ℵ₀ is the first uncountable cardinal, and so on. The notation ω_ combines the latter with Cardinal.ord, giving an enumeration of (infinite) initial ordinals. Thus ω_ 0 = ω and ω₁ = ω_ 1 is the first uncountable ordinal.
• The function Cardinal.beth enumerates the Beth cardinals. beth 0 = ℵ₀, beth (succ o) = 2 ^ beth o, and for a limit ordinal o, beth o is the supremum of beth a for a < o.

## Main Statements #

• Cardinal.mul_eq_max and Cardinal.add_eq_max state that the product (resp. sum) of two infinite cardinals is just their maximum. Several variations around this fact are also given.
• Cardinal.mk_list_eq_mk : when α is infinite, α and List α have the same cardinality.
• simp lemmas for inequalities between bit0 a and bit1 b are registered, making simp able to prove inequalities about numeral cardinals.

## Tags #

cardinal arithmetic (for infinite cardinals)

theorem Cardinal.ord_isLimit {c : Cardinal.{u_1}} (co : ) :
c.ord.IsLimit

### Aleph cardinals #

def Cardinal.alephIdx.initialSeg :
(fun (x x_1 : Cardinal.{u_1}) => x < x_1) ≼i fun (x x_1 : Ordinal.{u_1}) => x < x_1

The aleph' index function, which gives the ordinal index of a cardinal. (The aleph' part is because unlike aleph this counts also the finite stages. So alephIdx n = n, alephIdx ω = ω, alephIdx ℵ₁ = ω + 1 and so on.) In this definition, we register additionally that this function is an initial segment, i.e., it is order preserving and its range is an initial segment of the ordinals. For the basic function version, see alephIdx. For an upgraded version stating that the range is everything, see AlephIdx.rel_iso.

Equations
Instances For

The aleph' index function, which gives the ordinal index of a cardinal. (The aleph' part is because unlike aleph this counts also the finite stages. So alephIdx n = n, alephIdx ω = ω, alephIdx ℵ₁ = ω + 1 and so on.) For an upgraded version stating that the range is everything, see AlephIdx.rel_iso.

Equations
Instances For
@[simp]
theorem Cardinal.alephIdx_lt {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} :
a.alephIdx < b.alephIdx a < b
@[simp]
theorem Cardinal.alephIdx_le {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} :
a.alephIdx b.alephIdx a b
theorem Cardinal.alephIdx.init {a : Cardinal.{u_1}} {b : Ordinal.{u_1}} :
b < a.alephIdx∃ (c : Cardinal.{u_1}), c.alephIdx = b
def Cardinal.alephIdx.relIso :
(fun (x x_1 : Cardinal.{u}) => x < x_1) ≃r fun (x x_1 : Ordinal.{u}) => x < x_1

The aleph' index function, which gives the ordinal index of a cardinal. (The aleph' part is because unlike aleph this counts also the finite stages. So alephIdx n = n, alephIdx ℵ₀ = ω, alephIdx ℵ₁ = ω + 1 and so on.) In this version, we register additionally that this function is an order isomorphism between cardinals and ordinals. For the basic function version, see alephIdx.

Equations
Instances For
@[simp]
@[simp]
def Cardinal.Aleph'.relIso :
(fun (x x_1 : Ordinal.{u_1}) => x < x_1) ≃r fun (x x_1 : Cardinal.{u_1}) => x < x_1

The aleph' function gives the cardinals listed by their ordinal index, and is the inverse of aleph_idx. aleph' n = n, aleph' ω = ω, aleph' (ω + 1) = succ ℵ₀, etc. In this version, we register additionally that this function is an order isomorphism between ordinals and cardinals. For the basic function version, see aleph'.

Equations
Instances For

The aleph' function gives the cardinals listed by their ordinal index, and is the inverse of aleph_idx. aleph' n = n, aleph' ω = ω, aleph' (ω + 1) = succ ℵ₀, etc.

Equations
Instances For
@[simp]
@[simp]
theorem Cardinal.aleph'_lt {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :
o₁ < o₂
@[simp]
theorem Cardinal.aleph'_le {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :
o₁ o₂
@[simp]
theorem Cardinal.alephIdx_aleph' (o : Ordinal.{u_1}) :
().alephIdx = o
@[simp]
@[simp]
theorem Cardinal.aleph'_nat (n : ) :
= n
theorem Cardinal.aleph'_le_of_limit {o : Ordinal.{u_1}} (l : o.IsLimit) {c : Cardinal.{u_1}} :
o' < o, c
theorem Cardinal.aleph'_limit {o : Ordinal.{u_1}} (ho : o.IsLimit) :
= ⨆ (a : ()),
@[simp]

aleph' and aleph_idx form an equivalence between Ordinal and Cardinal

Equations
Instances For

The aleph function gives the infinite cardinals listed by their ordinal index. aleph 0 = ℵ₀, aleph 1 = succ ℵ₀ is the first uncountable cardinal, and so on.

Equations
Instances For
@[simp]
theorem Cardinal.aleph_lt {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :
o₁ < o₂
@[simp]
theorem Cardinal.aleph_le {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :
o₁ o₂
@[simp]
theorem Cardinal.max_aleph_eq (o₁ : Ordinal.{u_1}) (o₂ : Ordinal.{u_1}) :
max () () = Cardinal.aleph (max o₁ o₂)
@[simp]
theorem Cardinal.aleph_limit {o : Ordinal.{u_1}} (ho : o.IsLimit) :
= ⨆ (a : ()),
theorem Cardinal.aleph'_pos {o : Ordinal.{u_1}} (ho : 0 < o) :
@[simp]
theorem Cardinal.aleph_toNat (o : Ordinal.{u_1}) :
Cardinal.toNat () = 0
@[simp]
theorem Cardinal.aleph_toPartENat (o : Ordinal.{u_1}) :
Cardinal.toPartENat () =
Equations
• =
theorem Cardinal.ord_aleph_isLimit (o : Ordinal.{u_1}) :
().ord.IsLimit
theorem Cardinal.countable_iff_lt_aleph_one {α : Type u_1} (s : Set α) :
s.Countable
theorem Cardinal.ord_card_unbounded :
Set.Unbounded (fun (x x_1 : Ordinal.{u_1}) => x < x_1) {b : Ordinal.{u_1} | b.card.ord = b}

Ordinals that are cardinals are unbounded.

theorem Cardinal.eq_aleph'_of_eq_card_ord {o : Ordinal.{u_1}} (ho : o.card.ord = o) :
∃ (a : Ordinal.{u_1}), ().ord = o

ord ∘ aleph' enumerates the ordinals that are cardinals.

theorem Cardinal.ord_card_unbounded' :
Set.Unbounded (fun (x x_1 : Ordinal.{u_1}) => x < x_1) {b : Ordinal.{u_1} | b.card.ord = b }

Infinite ordinals that are cardinals are unbounded.

theorem Cardinal.eq_aleph_of_eq_card_ord {o : Ordinal.{u_1}} (ho : o.card.ord = o) (ho' : ) :
∃ (a : Ordinal.{u_1}), ().ord = o

ord ∘ aleph enumerates the infinite ordinals that are cardinals.

### Beth cardinals #

Beth numbers are defined so that beth 0 = ℵ₀, beth (succ o) = 2 ^ (beth o), and when o is a limit ordinal, beth o is the supremum of beth o' for o' < o.

Assuming the generalized continuum hypothesis, which is undecidable in ZFC, beth o = aleph o for every o.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
theorem Cardinal.beth_limit {o : Ordinal.{u_1}} :
o.IsLimit = ⨆ (a : ()),
@[simp]
theorem Cardinal.beth_lt {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :
o₁ < o₂
@[simp]
theorem Cardinal.beth_le {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :
o₁ o₂

### Properties of mul#

theorem Cardinal.mul_eq_self {c : Cardinal.{u_1}} (h : ) :
c * c = c

If α is an infinite type, then α × α and α have the same cardinality.

Properties of mul, not requiring ordinals

theorem Cardinal.mul_eq_max {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (ha : ) (hb : ) :
a * b = max a b

If α and β are infinite types, then the cardinality of α × β is the maximum of the cardinalities of α and β.

@[simp]
theorem Cardinal.mul_mk_eq_max {α : Type u} {β : Type u} [] [] :
= max () ()
@[simp]
@[simp]
theorem Cardinal.aleph0_mul_eq {a : Cardinal.{u_1}} (ha : ) :
@[simp]
theorem Cardinal.mul_aleph0_eq {a : Cardinal.{u_1}} (ha : ) :
theorem Cardinal.aleph0_mul_mk_eq {α : Type u_1} [] :
theorem Cardinal.mk_mul_aleph0_eq {α : Type u_1} [] :
theorem Cardinal.mul_lt_of_lt {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} (hc : ) (h1 : a < c) (h2 : b < c) :
a * b < c
theorem Cardinal.mul_eq_max_of_aleph0_le_left {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (h : ) (h' : b 0) :
a * b = max a b
theorem Cardinal.mul_eq_max' {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (h : ) :
a * b = max a b
theorem Cardinal.mul_eq_left {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (ha : ) (hb : b a) (hb' : b 0) :
a * b = a
theorem Cardinal.mul_eq_right {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (hb : ) (ha : a b) (ha' : a 0) :
a * b = b
theorem Cardinal.le_mul_left {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (h : b 0) :
a b * a
theorem Cardinal.le_mul_right {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (h : b 0) :
a a * b

### Properties of add#

theorem Cardinal.add_eq_self {c : Cardinal.{u_1}} (h : ) :
c + c = c

If α is an infinite type, then α ⊕ α and α have the same cardinality.

theorem Cardinal.add_eq_max {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (ha : ) :
a + b = max a b

If α is an infinite type, then the cardinality of α ⊕ β is the maximum of the cardinalities of α and β.

theorem Cardinal.add_eq_max' {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (ha : ) :
a + b = max a b
@[simp]
theorem Cardinal.add_mk_eq_max {α : Type u} {β : Type u} [] :
= max () ()
@[simp]
theorem Cardinal.add_mk_eq_max' {α : Type u} {β : Type u} [] :
= max () ()
theorem Cardinal.add_le_of_le {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} (hc : ) (h1 : a c) (h2 : b c) :
a + b c
theorem Cardinal.add_lt_of_lt {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} (hc : ) (h1 : a < c) (h2 : b < c) :
a + b < c
theorem Cardinal.eq_of_add_eq_of_aleph0_le {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} (h : a + b = c) (ha : a < c) (hc : ) :
b = c
theorem Cardinal.add_eq_left {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (ha : ) (hb : b a) :
a + b = a
theorem Cardinal.add_eq_right {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (hb : ) (ha : a b) :
a + b = b
theorem Cardinal.add_nat_eq {a : Cardinal.{u_1}} (n : ) (ha : ) :
a + n = a
theorem Cardinal.nat_add_eq {a : Cardinal.{u_1}} (n : ) (ha : ) :
n + a = a
theorem Cardinal.add_one_eq {a : Cardinal.{u_1}} (ha : ) :
a + 1 = a
theorem Cardinal.mk_add_one_eq {α : Type u_1} [] :
+ 1 =
theorem Cardinal.eq_of_add_eq_add_left {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} (h : a + b = a + c) (ha : ) :
b = c
theorem Cardinal.eq_of_add_eq_add_right {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} (h : a + b = c + b) (hb : ) :
a = c
theorem Cardinal.ciSup_add {ι : Type u} (f : ) [] (hf : ) (c : Cardinal.{v}) :
(⨆ (i : ι), f i) + c = ⨆ (i : ι), f i + c
theorem Cardinal.add_ciSup {ι : Type u} (f : ) [] (hf : ) (c : Cardinal.{v}) :
c + ⨆ (i : ι), f i = ⨆ (i : ι), c + f i
theorem Cardinal.ciSup_add_ciSup {ι : Type u} {ι' : Type w} (f : ) [] [Nonempty ι'] (hf : ) (g : ι'Cardinal.{v}) (hg : ) :
(⨆ (i : ι), f i) + ⨆ (j : ι'), g j = ⨆ (i : ι), ⨆ (j : ι'), f i + g j
theorem Cardinal.ciSup_mul {ι : Type u} (f : ) (c : Cardinal.{v}) :
(⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
theorem Cardinal.mul_ciSup {ι : Type u} (f : ) (c : Cardinal.{v}) :
c * ⨆ (i : ι), f i = ⨆ (i : ι), c * f i
theorem Cardinal.ciSup_mul_ciSup {ι : Type u} {ι' : Type w} (f : ) (g : ι'Cardinal.{v}) :
(⨆ (i : ι), f i) * ⨆ (j : ι'), g j = ⨆ (i : ι), ⨆ (j : ι'), f i * g j
@[simp]
theorem Cardinal.principal_add_ord {c : Cardinal.{u_1}} (hc : ) :
Ordinal.Principal (fun (x x_1 : Ordinal.{u_1}) => x + x_1) c.ord
theorem Cardinal.add_right_inj_of_lt_aleph0 {α : Cardinal.{u_1}} {β : Cardinal.{u_1}} {γ : Cardinal.{u_1}} (γ₀ : ) :
α + γ = β + γ α = β
@[simp]
theorem Cardinal.add_nat_inj {α : Cardinal.{u_1}} {β : Cardinal.{u_1}} (n : ) :
α + n = β + n α = β
@[simp]
theorem Cardinal.add_one_inj {α : Cardinal.{u_1}} {β : Cardinal.{u_1}} :
α + 1 = β + 1 α = β
theorem Cardinal.add_le_add_iff_of_lt_aleph0 {α : Cardinal.{u_1}} {β : Cardinal.{u_1}} {γ : Cardinal.{u_1}} (γ₀ : ) :
α + γ β + γ α β
@[simp]
theorem Cardinal.add_nat_le_add_nat_iff {α : Cardinal.{u_1}} {β : Cardinal.{u_1}} (n : ) :
α + n β + n α β
theorem Cardinal.add_nat_le_add_nat_iff_of_lt_aleph_0 {α : Cardinal.{u_1}} {β : Cardinal.{u_1}} (n : ) :
α + n β + n α β

Alias of Cardinal.add_nat_le_add_nat_iff.

@[simp]

Alias of Cardinal.add_one_le_add_one_iff.

theorem Cardinal.pow_le {κ : Cardinal.{u}} {μ : Cardinal.{u}} (H1 : ) (H2 : ) :
κ ^ μ κ
theorem Cardinal.pow_eq {κ : Cardinal.{u}} {μ : Cardinal.{u}} (H1 : ) (H2 : 1 μ) (H3 : ) :
κ ^ μ = κ
theorem Cardinal.power_self_eq {c : Cardinal.{u_1}} (h : ) :
c ^ c = 2 ^ c
theorem Cardinal.prod_eq_two_power {ι : Type u} [] {c : } (h₁ : ∀ (i : ι), 2 c i) (h₂ : ∀ (i : ι), Cardinal.lift.{u, v} (c i) ) :
= 2 ^
theorem Cardinal.power_eq_two_power {c₁ : Cardinal.{u_1}} {c₂ : Cardinal.{u_1}} (h₁ : ) (h₂ : 2 c₂) (h₂' : c₂ c₁) :
c₂ ^ c₁ = 2 ^ c₁
theorem Cardinal.nat_power_eq {c : Cardinal.{u}} (h : ) {n : } (hn : 2 n) :
n ^ c = 2 ^ c
theorem Cardinal.power_nat_le {c : Cardinal.{u}} {n : } (h : ) :
c ^ n c
theorem Cardinal.power_nat_eq {c : Cardinal.{u}} {n : } (h1 : ) (h2 : 1 n) :
c ^ n = c

### Computing cardinality of various types #

theorem Cardinal.mk_equiv_eq_zero_iff_ne {α : Type u} {β : Type u} :
Cardinal.mk (α β) = 0
theorem Cardinal.mk_equiv_comm {α : Type u} {β' : Type v} :
Cardinal.mk (α β') = Cardinal.mk (β' α)

This lemma makes lemmas assuming Infinite α applicable to the situation where we have Infinite β instead.

theorem Cardinal.mk_arrow_eq_zero_iff {α : Type u} {β' : Type v} :
Cardinal.mk (αβ') = 0 0 = 0
theorem Cardinal.mk_surjective_eq_zero_iff_lift {α : Type u} {β' : Type v} :
Cardinal.mk {f : αβ' | } = 0 < 0 = 0
theorem Cardinal.mk_surjective_eq_zero_iff {α : Type u} {β : Type u} :
Cardinal.mk {f : αβ | } = 0 0 = 0
theorem Cardinal.mk_equiv_le_embedding (α : Type u) (β' : Type v) :
Cardinal.mk (α β') Cardinal.mk (α β')
theorem Cardinal.mk_embedding_le_arrow (α : Type u) (β' : Type v) :
Cardinal.mk (α β') Cardinal.mk (αβ')
theorem Cardinal.mk_perm_eq_two_power {α : Type u} [] :
= 2 ^
theorem Cardinal.mk_equiv_eq_arrow_of_lift_eq {α : Type u} {β' : Type v} [] (leq : = ) :
Cardinal.mk (α β') = Cardinal.mk (αβ')
theorem Cardinal.mk_equiv_eq_arrow_of_eq {α : Type u} {β : Type u} [] (eq : ) :
Cardinal.mk (α β) = Cardinal.mk (αβ)
theorem Cardinal.mk_equiv_of_lift_eq {α : Type u} {β' : Type v} [] (leq : = ) :
Cardinal.mk (α β') = 2 ^
theorem Cardinal.mk_equiv_of_eq {α : Type u} {β : Type u} [] (eq : ) :
Cardinal.mk (α β) = 2 ^
theorem Cardinal.mk_embedding_eq_arrow_of_lift_le {α : Type u} {β' : Type v} [] (lle : ) :
Cardinal.mk (β' α) = Cardinal.mk (β'α)
theorem Cardinal.mk_embedding_eq_arrow_of_le {α : Type u} {β : Type u} [] (le : ) :
Cardinal.mk (β α) = Cardinal.mk (βα)
theorem Cardinal.mk_surjective_eq_arrow_of_lift_le {α : Type u} {β' : Type v} [] (lle : ) :
Cardinal.mk {f : αβ' | } = Cardinal.mk (αβ')
theorem Cardinal.mk_surjective_eq_arrow_of_le {α : Type u} {β : Type u} [] (le : ) :
Cardinal.mk {f : αβ | } = Cardinal.mk (αβ)
@[simp]
theorem Cardinal.mk_list_eq_mk (α : Type u) [] :
theorem Cardinal.mk_list_eq_aleph0 (α : Type u) [] [] :
@[simp]
theorem Cardinal.mk_finset_of_infinite (α : Type u) [] :
@[simp]
theorem Cardinal.mk_finsupp_lift_of_infinite (α : Type u) (β : Type v) [] [Zero β] [] :
Cardinal.mk (α →₀ β) = max () ()
theorem Cardinal.mk_finsupp_of_infinite (α : Type u) (β : Type u) [] [Zero β] [] :
Cardinal.mk (α →₀ β) = max () ()
@[simp]
theorem Cardinal.mk_finsupp_lift_of_infinite' (α : Type u) (β : Type v) [] [Zero β] [] :
Cardinal.mk (α →₀ β) = max () ()
theorem Cardinal.mk_finsupp_of_infinite' (α : Type u) (β : Type u) [] [Zero β] [] :
Cardinal.mk (α →₀ β) = max () ()
@[simp]
theorem Cardinal.mk_bounded_set_le (α : Type u) (c : Cardinal.{u}) :
Cardinal.mk { t : Set α // c }
theorem Cardinal.mk_bounded_subset_le {α : Type u} (s : Set α) (c : Cardinal.{u}) :
Cardinal.mk { t : Set α // t s c } ^ c

### Properties of compl#

theorem Cardinal.mk_compl_of_infinite {α : Type u_1} [] (s : Set α) (h2 : ) :
theorem Cardinal.mk_compl_finset_of_infinite {α : Type u_1} [] (s : ) :
Cardinal.mk (s) =
theorem Cardinal.mk_compl_eq_mk_compl_infinite {α : Type u_1} [] {s : Set α} {t : Set α} (hs : ) (ht : ) :
theorem Cardinal.mk_compl_eq_mk_compl_finite_lift {α : Type u} {β : Type v} [] {s : Set α} {t : Set β} (h1 : = ) (h2 : = ) :
=
theorem Cardinal.mk_compl_eq_mk_compl_finite {α : Type u} {β : Type u} [] {s : Set α} {t : Set β} (h1 : ) (h : = ) :
theorem Cardinal.mk_compl_eq_mk_compl_finite_same {α : Type u} [] {s : Set α} {t : Set α} (h : = ) :

### Extending an injection to an equiv #

theorem Cardinal.extend_function {α : Type u_1} {β : Type u_2} {s : Set α} (f : s β) (h : Nonempty (s ())) :
∃ (g : α β), ∀ (x : s), g x = f x
theorem Cardinal.extend_function_finite {α : Type u} {β : Type v} [] {s : Set α} (f : s β) (h : Nonempty (α β)) :
∃ (g : α β), ∀ (x : s), g x = f x
theorem Cardinal.extend_function_of_lt {α : Type u_1} {β : Type u_2} {s : Set α} (f : s β) (hs : ) (h : Nonempty (α β)) :
∃ (g : α β), ∀ (x : s), g x = f x

ω_ o is a notation for the initial ordinal of cardinality aleph o. Thus, for example ω_ 0 = ω.

Equations
Instances For

ω₁ is the first uncountable ordinal.

Equations
Instances For

### Cardinal operations with ordinal indices #

Results on cardinality of ordinal-indexed families of sets.

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 : ) (A : ) (hA : j < o, Cardinal.mk (A j) c) :
Cardinal.mk (⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < o), A j) c

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