Theorems · Definition · logic and foundations

Cardinal.aleph

Ordinal.{u_1} ↪o Cardinal.{u_1}

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.

Defined in

Mathlib.SetTheory.Cardinal.Aleph

Cited by

76 results in Mathlib

Foundations

Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound