toNatOrdinal_toOrdinal — Mathlib

English

For every ordinal a, converting to a NatOrdinal and back to an ordinal yields the original ordinal.

Русский

Для каждого ординала a преобразование к NatOrdinal и последующее преобразование обратно к ординалу даёт исходный ординал.

LaTeX

$$$toNatOrdinal(a).toOrdinal = a$$$

Lean4

@[simp]
theorem toNatOrdinal_toOrdinal (a : Ordinal) : a.toNatOrdinal.toOrdinal = a :=
  rfl

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