fintypeRightMoves

Mathlib.SetTheory.Game.Short

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

English

For any short game, the RightMoves form a finite type.

Русский

Для любой короткой игры множество правых ходов образует конечный тип.

LaTeX

$$$ \forall x \,[Short(x) \Rightarrow Fintype(x.RightMoves)]$$$

Lean4

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

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

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

Разделы

Аффилиация

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