toOrdinal_toNatOrdinal

Mathlib.SetTheory.Ordinal.NaturalOps

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

English

Applying toOrdinal and then toNatOrdinal yields the original NatOrdinal: a.toOrdinal.toNatOrdinal = a.

Русский

Применение toOrdinal, а затем toNatOrdinal возвращает исходный NatOrdinal: a.toOrdinal.toNatOrdinal = a.

LaTeX

$$$\\mathrm{toNatOrdinal}(\\mathrm{toOrdinal}(a)) = a$$$

Lean4

@[simp]
theorem toOrdinal_toNatOrdinal (a : NatOrdinal) : a.toOrdinal.toNatOrdinal = a :=
  rfl

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

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

Разделы

Аффилиация

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