aleph — Mathlib

English

For all ordinals o1, o2, we have ℵ_{max(o1,o2)} = max(ℵ_{o1}, ℵ_{o2}).

Русский

Для любых ординалов o1, o2 выполняется ℵ_{max(o1,o2)} = max(ℵ_{o1}, ℵ_{o2}).

LaTeX

$$$$ \aleph_{\max(o_1,o_2)} = \max(\aleph_{o_1}, \aleph_{o_2}). $$$$

Lean4

/-- 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`. -/
def aleph : Ordinal ↪o Cardinal :=
  (OrderEmbedding.addLeft ω).trans preAleph.toOrderEmbedding

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