Theorems · Definition · logic and foundations

Cardinal.preAleph

Ordinal.{u} ≃o Cardinal.{u}

The "pre-aleph" function gives the cardinals listed by their ordinal index. preAleph n = n, preAleph ω = ℵ₀, preAleph (ω + 1) = succ ℵ₀, etc. For the more common aleph function skipping over finite cardinals, see Cardinal.aleph.

Defined in

Mathlib.SetTheory.Cardinal.Aleph

Cited by

44 results in Mathlib

Foundations

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