toNimber_toOrdinal

Mathlib.SetTheory.Nimber.Basic

URI: https://scilib.ai/kg/mathlib#Ordinal.toNimber_toOrdinal

English

The composite of the toNimber map followed by its inverse toOrdinal returns the original ordinal.

Русский

Композиция отображения к Nimber и его обратного отображения к Ordinal возвращает исходный ординал.

LaTeX

$$$\\\\forall a \\\\in \\\\mathrm{Ordinal},\\\\ toOrdinal( toNimber(a) ) = a.$$$

Lean4

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

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

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

Разделы

Аффилиация

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