Cardinals

DefinitionCardinal#

Cardinal.{u} is the type of cardinal numbers in Type u, defined as the quotient of Type u by existence of an equivalence (a bijection with explicit inverse).

Cardinal.{u} : Type (u + 1)
Sources
MathlibCardinal
Used by 39
Used byThe Non-Denumerability of the Continuum · Minkowski’s Fundamental Theorem · Finite-dimensional normed spaces over complete normed fields are complete · Heine-Borel theorem (finite-dimensional normed spaces are proper) · Cauchy-Davenport theorem · Ruzsa covering lemma · Regularity lemma · Small category · Sphere · Diagonalization of self-adjoint endomorphisms · Löwenheim-Skolem · Beth numbers · Cofinality · Binomial law · Dimension theorem for vector spaces · Rank–nullity theorem · Focal subgroup theorem · Wedderburn–Artin theorem · Lie's theorem · Schur–Zassenhaus theorem · Schur's lemma (1000+ theorems) · Tutte theorem · König's theorem (set theory) · Well-ordering theorem · Intersecting secants theorem · Helly's theorem · Whitney embedding theorem · Cocyclicity · Inscribed angle theorem · Adjoint endomorphism · Complex classification · Sylvester's law of inertia (existence) · Sylvester's law of inertia (uniqueness) · Rank of a linear map · Rank of a set of vectors · Schur's lemma (Linear representations) · Rank of a matrix · Cauchy formulas · Continuity (continuity and differentiability of convex functions)

DefinitionAleph numbers#

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.preAleph.

Conventions for notations in identifiers:

  • The recommended spelling of ℵ_ in identifiers is aleph.
Cardinal.aleph.{u_1} : Ordinal.{u_1} ↪o Cardinal.{u_1}
Sources
MathlibCardinal.aleph
Uses 3
Statement usesCofinality · Natural number · Ordinal

DefinitionBeth numbers#

The Beth function is defined so that beth 0 = ℵ₀, beth (succ o) = 2 ^ beth o, and that for a limit ordinal o, beth o is the supremum of beth a for a < o.

Assuming the generalized continuum hypothesis, which is undecidable in ZFC, we have ℶ_ o = ℵ_ o for all ordinals.

For a version which starts at zero, see Cardinal.preBeth.

Cardinal.beth.{u} (o : Ordinal.{u}) : Cardinal.{u}
Sources
MathlibCardinal.beth
Uses 3
Statement usesCardinal · Natural number · Ordinal

DefinitionCofinality#

The cofinality of a preorder is the smallest cardinality of a cofinal subset.

Order.cof.{u} (α : Type u) [Preorder α] : Cardinal.{u}
Sources
MathlibOrder.cof
Uses 2 · Used by 2
Statement usesCardinal · Set
Used byAleph numbers · Fundamental sequences

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.