toOrdinal_symm_eq

Mathlib.SetTheory.Ordinal.NaturalOps

URI: https://scilib.ai/kg/mathlib#NatOrdinal.toOrdinal_symm_eq

English

The inverse of toOrdinal equals toNatOrdinal; i.e., the two canonical identifications are inverse to each other.

Русский

Обратная к toOrdinal равна toNatOrdinal; канонические идентификации являются взаимно обратными.

LaTeX

$$$\\mathrm{toOrdinal}^{-1} = \\mathrm{toNatOrdinal}$$$

Lean4

@[simp]
theorem toOrdinal_symm_eq : NatOrdinal.toOrdinal.symm = Ordinal.toNatOrdinal :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru