toNimber_symm_eq — Mathlib

English

The natural isomorphism between the ordinal and nimber frameworks has inverse given by the other natural embedding; i.e., toNimber.symm equals toOrdinal.

Русский

Естественный изоморфизм между порядковым и нимберным подходами имеет обратное отображение, равное противоположному вложению; то есть toNimber.symm = Nimber.toOrdinal.

LaTeX

$$$\\operatorname{toNimber}^{-1} = \\operatorname{toOrdinal}.$$$

Lean4

@[simp]
theorem toNimber_symm_eq : toNimber.symm = Nimber.toOrdinal :=
  rfl

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