Cardinals and ordinals
Relationships between cardinals and ordinals, properties of cardinals that are proved using ordinals.
Main definitions and results
- The
aleph'function gives the cardinals listed by their ordinal index, and is the inverse ofaleph_idx.aleph' n = n,aleph' ω = ω,aleph' (ω + 1) = ℵ₁, etc. It is an order isomorphism between ordinals and cardinals. The
alephfunction gives the infinite cardinals listed by their ordinal index.aleph 0 = ω,aleph 1 = succ ωis the first uncountable cardinal, and so on.mul_eq_maxandadd_eq_maxstate that the product (resp. sum) of two infinite cardinals is just their maximum. Several variations around this fact are also given.mk_list_eq_mk: whenαis infinite,αandlist αhave the same cardinality.- simp lemmas for inequalities between
bit0 aandbit1 bare registered, making simp able to prove inequalities about numeral cardinals.
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.
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.
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
- cardinal.aleph_idx.rel_iso = rel_iso.of_surjective ↑cardinal.aleph_idx.initial_seg cardinal.aleph_idx.rel_iso._proof_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) = ℵ₁, 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'.
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
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
Properties of mul
If α is an infinite type, then α × α and α have the same cardinality.
If α and β are infinite types, then the cardinality of α × β is the maximum
of the cardinalities of α and β.
Properties of add
If α is an infinite type, then α ⊕ α and α have the same cardinality.
If α is an infinite type, then the cardinality of α ⊕ β is the maximum
of the cardinalities of α and β.
Properties about power
Computing cardinality of various types
Properties of compl
Extending an injection to an equiv
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 }