preAleph — Mathlib

English

As above, simplified form of membership criterion.

Русский

Как выше, упрощённая форма критерия членства.

LaTeX

$$$ x \in \operatorname{range}(\omega) \iff \omega \le x \land IsInitial(x) $$$

Lean4

/-- 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`. -/
def preAleph : Ordinal.{u} ≃o Cardinal.{u} :=
  (enumOrdOrderIso _ not_bddAbove_isInitial).trans isInitialIso

Похожие утверждения