toOrdinal_toNimber — Mathlib

English

For every nimber a, applying the ordinal embedding to a and then reinterpreting it as a nimber yields the original nimber: toNimber(toOrdinal(a)) = a.

Русский

Для любого нембера a применение отображения из Nimber в Ordinal, а затем обратное преобразование обратно в Nimber даёт исходный нембер: toNimber(toOrdinal(a)) = a.

LaTeX

$$$\operatorname{toNimber}(\operatorname{toOrdinal}(a)) = a$$$

Lean4

@[simp]
theorem toOrdinal_toNimber (a : Nimber) : ∗(Nimber.toOrdinal a) = a :=
  rfl

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