instNatCast

Mathlib.SetTheory.PGame.Algebra

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.instNatCast

Lean4

/-- The pre-game `((0 + 1) + ⋯) + 1`.

Note that this is **not** the usual recursive definition `n = {0, 1, … | }`. For instance,
`2 = 0 + 1 + 1 = {0 + 0 + 1, 0 + 1 + 0 | }` does not contain any left option equivalent to `0`. For
an implementation of said definition, see `Ordinal.toPGame`. For the proof that these games are
equivalent, see `Ordinal.toPGame_natCast`. -/
instance : NatCast PGame :=
  ⟨Nat.unaryCast⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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