English
There is an order-preserving embedding e from Cardinals to Ordinals such that e(c) is the least ordinal with cardinality c for every cardinal c.
Русский
Существуют упорядоченно-инвариантное вложение e: Cardinal → Ordinal, такое что для каждого кардинала c минимальный ординал с кардинальностью c равен e(c).
LaTeX
$$$\\exists e:\\mathrm{Cardinal} \\hookrightarrow\\mathrm{Ordinal}\\text{ with }\\forall c:\\mathrm{Cardinal},\\; \\operatorname{card}(e(c)) = c \\land \\forall \\alpha\\,(\\operatorname{card}(\\alpha) = c \\rightarrow e(c) \\le \\alpha).$$$
Lean4
/-- The ordinal corresponding to a cardinal `c` is the least ordinal
whose cardinal is `c`. This is the order-embedding version. For the regular function, see `ord`.
-/
def orderEmbedding : Cardinal ↪o Ordinal :=
RelEmbedding.orderEmbeddingOfLTEmbedding (RelEmbedding.ofMonotone Cardinal.ord fun _ _ => Cardinal.ord_lt_ord.2)
