mathlib documentation

set_theory.cardinal_ordinal

Cardinals and ordinals

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

Main definitions and results

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 aleph_idx n = n, aleph_idx ω = ω, aleph_idx ℵ₁ = ω + 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 aleph_idx. For an upgraded version stating that the range is everything, see aleph_idx.rel_iso.

Equations

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 aleph_idx n = n, aleph_idx ω = ω, aleph_idx ℵ₁ = ω + 1 and so on.) For an upgraded version stating that the range is everything, see aleph_idx.rel_iso.

Equations
@[simp]
theorem cardinal.aleph_idx_lt {a b : cardinal} :

@[simp]

theorem cardinal.aleph_idx.init {a : cardinal} {b : ordinal} :
b < a.aleph_idx(∃ (c : cardinal), c.aleph_idx = b)

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 aleph_idx n = n, aleph_idx ω = ω, aleph_idx ℵ₁ = ω + 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 aleph_idx.

Equations

The aleph' function gives the cardinals listed by their ordinal index, and is the inverse of aleph_idx. aleph' n = n, aleph' ω = ω, aleph' (ω + 1) = ℵ₁, 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

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

Equations
@[simp]
theorem cardinal.aleph'_lt {o₁ o₂ : ordinal} :
cardinal.aleph' o₁ < cardinal.aleph' o₂ o₁ < o₂

@[simp]
theorem cardinal.aleph'_le {o₁ o₂ : ordinal} :

@[simp]

@[simp]

theorem cardinal.aleph'_le_of_limit {o : ordinal} (l : o.is_limit) {c : cardinal} :
cardinal.aleph' o c ∀ (o' : ordinal), o' < ocardinal.aleph' o' c

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
@[simp]
theorem cardinal.aleph_lt {o₁ o₂ : ordinal} :
cardinal.aleph o₁ < cardinal.aleph o₂ o₁ < o₂

@[simp]
theorem cardinal.aleph_le {o₁ o₂ : ordinal} :

Properties of mul

theorem cardinal.mul_eq_self {c : cardinal} :
cardinal.omega cc * c = c

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

theorem cardinal.mul_eq_max {a b : cardinal} :
cardinal.omega acardinal.omega ba * b = max a b

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

theorem cardinal.mul_lt_of_lt {a b c : cardinal} :
cardinal.omega ca < cb < ca * b < c

theorem cardinal.mul_eq_max_of_omega_le_left {a b : cardinal} :
cardinal.omega ab 0a * b = max a b

theorem cardinal.mul_eq_left {a b : cardinal} :
cardinal.omega ab ab 0a * b = a

theorem cardinal.mul_eq_right {a b : cardinal} :
cardinal.omega ba ba 0a * b = b

theorem cardinal.le_mul_left {a b : cardinal} :
b 0a b * a

theorem cardinal.le_mul_right {a b : cardinal} :
b 0a a * b

theorem cardinal.mul_eq_left_iff {a b : cardinal} :
a * b = a max cardinal.omega b a b 0 b = 1 a = 0

Properties of add

theorem cardinal.add_eq_self {c : cardinal} :
cardinal.omega cc + c = c

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

theorem cardinal.add_eq_max {a b : cardinal} :
cardinal.omega aa + b = max a b

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

theorem cardinal.add_lt_of_lt {a b c : cardinal} :
cardinal.omega ca < cb < ca + b < c

theorem cardinal.eq_of_add_eq_of_omega_le {a b c : cardinal} :
a + b = ca < ccardinal.omega cb = c

theorem cardinal.add_eq_left {a b : cardinal} :
cardinal.omega ab aa + b = a

theorem cardinal.add_eq_right {a b : cardinal} :
cardinal.omega ba ba + b = b

theorem cardinal.add_eq_left_iff {a b : cardinal} :
a + b = a max cardinal.omega b a b = 0

theorem cardinal.add_one_eq {a : cardinal} :
cardinal.omega aa + 1 = a

theorem cardinal.eq_of_add_eq_add_left {a b c : cardinal} :
a + b = a + ca < cardinal.omegab = c

theorem cardinal.eq_of_add_eq_add_right {a b c : cardinal} :
a + b = c + bb < cardinal.omegaa = c

Properties about power

theorem cardinal.pow_le {κ μ : cardinal} :
cardinal.omega κμ < cardinal.omegaκ ^ μ κ

theorem cardinal.power_self_eq {c : cardinal} :
cardinal.omega cc ^ c = 2 ^ c

theorem cardinal.power_nat_le {c : cardinal} {n : } :

Computing cardinality of various types

theorem cardinal.mk_list_eq_mk {α : Type u} :
cardinal.omega # α# (list α) = # α

theorem cardinal.mk_finset_eq_mk {α : Type u} :
cardinal.omega # α# (finset α) = # α

theorem cardinal.mk_bounded_set_le_of_omega_le (α : Type u) (c : cardinal) :
cardinal.omega # α# {t // # t c} # α ^ c

theorem cardinal.mk_bounded_set_le (α : Type u) (c : cardinal) :
# {t // # t c} max (# α) cardinal.omega ^ c

theorem cardinal.mk_bounded_subset_le {α : Type u} (s : set α) (c : cardinal) :
# {t // t s # t c} max (# s) cardinal.omega ^ c

Properties of compl

theorem cardinal.mk_compl_of_omega_le {α : Type u_1} (s : set α) :
cardinal.omega # α# s < # α# s = # α

theorem cardinal.mk_compl_finset_of_omega_le {α : Type u_1} (s : finset α) :

theorem cardinal.mk_compl_eq_mk_compl_infinite {α : Type u_1} {s t : set α} :
cardinal.omega # α# s < # α# t < # α# s = # t

theorem cardinal.mk_compl_eq_mk_compl_finite_lift {α : Type u} {β : Type v} {s : set α} {t : set β} :
# α < cardinal.omega(# α).lift = (# β).lift(# s).lift = (# t).lift(# s).lift = (# t).lift

theorem cardinal.mk_compl_eq_mk_compl_finite {α β : Type u} {s : set α} {t : set β} :
# α < cardinal.omega# α = # β# s = # t# s = # t

theorem cardinal.mk_compl_eq_mk_compl_finite_same {α : Type u_1} {s t : set α} :
# α < cardinal.omega# s = # t# s = # t

Extending an injection to an equiv

theorem cardinal.extend_function {α : Type u_1} {β : Type u_2} {s : set α} (f : s β) :
nonempty (s (set.range f))(∃ (g : α β), ∀ (x : s), g x = f x)

theorem cardinal.extend_function_finite {α : Type u_1} {β : Type u_2} {s : set α} (f : s β) :
# α < cardinal.omeganonempty β)(∃ (g : α β), ∀ (x : s), g x = f x)

theorem cardinal.extend_function_of_lt {α : Type u_1} {β : Type u_2} {s : set α} (f : s β) :
# s < # αnonempty β)(∃ (g : α β), ∀ (x : s), g x = f x)

This section proves inequalities for bit0 and bit1, enabling simp to solve inequalities for numeral cardinals. The complexity of the resulting algorithm is not good, as in some cases simp reduces an inequality to a disjunction of two situations, depending on whether a cardinal is finite or infinite. Since the evaluation of the branches is not lazy, this is bad. It is good enough for practical situations, though.

For specific numbers, these inequalities could also be deduced from the corresponding inequalities of natural numbers using norm_cast:

example : (37 : cardinal) < 42 :=
by { norm_cast, norm_num }
@[simp]
theorem cardinal.bit0_ne_zero (a : cardinal) :
¬bit0 a = 0 ¬a = 0

@[simp]
theorem cardinal.bit1_ne_zero (a : cardinal) :
¬bit1 a = 0

@[simp]
theorem cardinal.zero_lt_bit0 (a : cardinal) :
0 < bit0 a 0 < a

@[simp]
theorem cardinal.zero_lt_bit1 (a : cardinal) :
0 < bit1 a

@[simp]
theorem cardinal.one_le_bit0 (a : cardinal) :
1 bit0 a 0 < a

@[simp]
theorem cardinal.one_le_bit1 (a : cardinal) :
1 bit1 a

@[simp]
theorem cardinal.bit0_le_bit0 {a b : cardinal} :
bit0 a bit0 b a b

@[simp]
theorem cardinal.bit0_le_bit1 {a b : cardinal} :
bit0 a bit1 b a b

@[simp]
theorem cardinal.bit1_le_bit1 {a b : cardinal} :
bit1 a bit1 b a b

@[simp]

@[simp]
theorem cardinal.bit0_lt_bit0 {a b : cardinal} :
bit0 a < bit0 b a < b

@[simp]
theorem cardinal.bit1_lt_bit0 {a b : cardinal} :
bit1 a < bit0 b a < b

@[simp]
theorem cardinal.bit1_lt_bit1 {a b : cardinal} :
bit1 a < bit1 b a < b

@[simp]
theorem cardinal.bit0_lt_bit1 {a b : cardinal} :

theorem cardinal.one_lt_two  :
1 < 2

@[simp]
theorem cardinal.one_lt_bit0 {a : cardinal} :
1 < bit0 a 0 < a

@[simp]
theorem cardinal.one_lt_bit1 (a : cardinal) :
1 < bit1 a 0 < a

@[simp]
theorem cardinal.one_le_one  :
1 1