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 ofCardinal.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 withCardinal.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 ordinalo
,beth o
is the supremum ofbeth a
fora < o
.
Main Statements #
Cardinal.mul_eq_max
andCardinal.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,α
andList α
have the same cardinality.- simp lemmas for inequalities between
bit0 a
andbit1 b
are registered, makingsimp
able to prove inequalities about numeral cardinals.
Tags #
cardinal arithmetic (for infinite cardinals)
Aleph 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 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
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
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
Ordinals that are cardinals are unbounded.
ord ∘ aleph'
enumerates the ordinals that are cardinals.
Infinite ordinals that are cardinals are unbounded.
ord ∘ aleph
enumerates the infinite ordinals that are cardinals.
Beth cardinals #
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 #
ω_ o
is a notation for the initial ordinal of cardinality
aleph o
. Thus, for example ω_ 0 = ω
.
Instances For
Cardinal operations with ordinal indices #
Results on cardinality of ordinal-indexed families of sets.
Bounding the cardinal of an ordinal-indexed union of sets.