shortNat

Mathlib.SetTheory.Game.Short

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

English

Natural numbers, viewed as PGames via their standard construction, are short.

Русский

Натуральные числа, как игры PGame через стандартное построение, являются короткими.

LaTeX

$$$\forall n \in \mathbb{N}, Short(n)$$$

Lean4

instance shortNat : ∀ n : ℕ, Short n
  | 0 => PGame.short0
  | n + 1 => @PGame.shortAdd _ _ (shortNat n) PGame.short1

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

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

Разделы

Аффилиация

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