fintypeLeftMoves

Mathlib.SetTheory.Game.Short

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

English

Every short PGame has a finite set of LeftMoves.

Русский

У каждой короткой PGame конечен набор левых ходов.

LaTeX

$$$ Short(x) \Rightarrow \#(x.LeftMoves) < \infty $$$

Lean4

instance fintypeLeftMoves (x : PGame) [S : Short x] : Fintype x.LeftMoves := by cases S; assumption

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

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

Разделы

Аффилиация

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