# Documentation

Mathlib.SetTheory.Cardinal.Ordinal

# 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)

### Aleph cardinals #

def Cardinal.alephIdx.initialSeg :
(fun x x_1 => x < x_1) ≼i fun x x_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.

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.

Instances For
def Cardinal.alephIdx.relIso :
(fun x x_1 => x < x_1) ≃r fun x x_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 version, we register additionally that this function is an order isomorphism between cardinals and ordinals. For the basic function version, see alephIdx.

Instances For
@[simp]
@[simp]
theorem Cardinal.type_cardinal :
(Ordinal.type fun x x_1 => x < x_1) = Ordinal.univ
@[simp]
def Cardinal.Aleph'.relIso :
(fun x x_1 => x < x_1) ≃r fun x x_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'.

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.

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]
@[simp]
theorem Cardinal.aleph'_nat (n : ) :
= n
theorem Cardinal.aleph'_le_of_limit {o : Ordinal.{u_1}} (l : ) {c : Cardinal.{u_1}} :
∀ (o' : Ordinal.{u_1}), o' < o c
theorem Cardinal.aleph'_limit {o : Ordinal.{u_1}} (ho : ) :
= ⨆ (a : ↑()),
@[simp]

aleph' and aleph_idx form an equivalence between Ordinal and Cardinal

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.

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 : ) :
= ⨆ (a : ↑()),
theorem Cardinal.aleph'_pos {o : Ordinal.{u_1}} (ho : 0 < o) :
theorem Cardinal.countable_iff_lt_aleph_one {α : Type u_1} (s : Set α) :
theorem Cardinal.ord_card_unbounded :
Set.Unbounded (fun x x_1 => x < x_1) {b | }

Ordinals that are cardinals are unbounded.

ord ∘ aleph' enumerates the ordinals that are cardinals.

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

Infinite ordinals that are cardinals are unbounded.

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

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.

Instances For
@[simp]
@[simp]
theorem Cardinal.beth_limit {o : Ordinal.{u_1}} :
= ⨆ (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.

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_1} {β : Type u_1} [] [] :
= 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_1} {β : Type u_1} [] :
= max () ()
@[simp]
theorem Cardinal.add_mk_eq_max' {α : Type u_1} {β : Type u_1} [] :
= 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.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
@[simp]
theorem Cardinal.principal_add_ord {c : Cardinal.{u_1}} (hc : ) :
Ordinal.Principal (fun x x_1 => x + x_1) ()
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_of_lt_aleph_0 {α : Cardinal.{u_1}} {β : Cardinal.{u_1}} (n : ) :
α + n β + n α β

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 #

@[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]
@[simp]
theorem Cardinal.mk_multiset_of_isEmpty (α : Type u) [] :
= 1
theorem Cardinal.mk_bounded_subset_le {α : Type u} (s : Set α) (c : Cardinal.{u}) :
Cardinal.mk { t // 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 = ω.

Instances For

ω₁ is the first uncountable ordinal.

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 : ) (hc : ) (A : ) (hA : ∀ (j : Ordinal.{u_1}), j < oCardinal.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.