nat_succ

Mathlib.SetTheory.PGame.Algebra

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

English

The natural-number embedding preserves successor: (n+1) as a P-Game equals n+1.

Русский

Встроение натурального числа в PGame сохраняет операцию следующего элемента: n+1 равно n+1 как игра.

LaTeX

$$$(n+1) \\text{: PGame} = n+1$$$

Lean4

@[simp]
protected theorem nat_succ (n : ℕ) : ((n + 1 : ℕ) : PGame) = n + 1 :=
  rfl

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

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

Разделы

Аффилиация

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