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.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.
Tags #
cardinal arithmetic (for infinite cardinals)
Aleph cardinals #
The aleph'
function gives the cardinals listed by their ordinal index. aleph' n = n
,
aleph' ω = ℵ₀
, aleph' (ω + 1) = succ ℵ₀
, etc.
For the more common aleph function skipping over finite cardinals, see Cardinal.aleph
.
Equations
- Cardinal.aleph' = (OrderIso.ofRelIsoLT (RelIso.ofSurjective Cardinal.ord.orderEmbedding.ltEmbedding.collapse.toRelEmbedding Cardinal.aleph'.proof_1)).symm
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 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
- Cardinal.alephIdx.initialSeg = Cardinal.ord.orderEmbedding.ltEmbedding.collapse
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
.
Equations
- Cardinal.alephIdx.relIso = Cardinal.aleph'.symm.toRelIsoLT
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
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
Alias of Cardinal.aleph'_omega0
.
aleph'
and aleph_idx
form an equivalence between Ordinal
and Cardinal
Equations
- Cardinal.aleph'Equiv = { toFun := ⇑Cardinal.aleph', invFun := Cardinal.alephIdx, left_inv := Cardinal.alephIdx_aleph', right_inv := Cardinal.aleph'_alephIdx }
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.
For a version including finite cardinals, see Cardinal.aleph'
.
Equations
- Cardinal.aleph = RelEmbedding.trans (OrderEmbedding.addLeft Ordinal.omega0) Cardinal.aleph'.toOrderEmbedding
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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 #
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
Properties of mul
#
If α
is an infinite type, then α × α
and α
have the same cardinality.
Properties of mul
, not requiring ordinals
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 β
.
Alias of Cardinal.add_nat_le_add_nat_iff
.
Alias of Cardinal.add_one_le_add_one_iff
.
Properties about power #
Computing cardinality of various types #
This lemma makes lemmas assuming Infinite α
applicable to the situation where we have
Infinite β
instead.
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 = ω
.
Equations
- Ordinal.termω__ = Lean.ParserDescr.node `Ordinal.termω__ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ω_") (Lean.ParserDescr.cat `term 0))
Instances For
ω₁
is the first uncountable ordinal.
Equations
- Ordinal.termω₁ = Lean.ParserDescr.node `Ordinal.termω₁ 1024 (Lean.ParserDescr.symbol "ω₁")
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.