isEmpty

Mathlib.SetTheory.PGame.Order

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

English

If a pre-game has no moves for either player, it is equivalent to 0.

Русский

Если у предигры нет ходов ни у одного игрока, она эквивалентна нулю.

LaTeX

$$$x \\,\\approx\\, 0 \\\\text{ if } x.LeftMoves = \\varnothing \\\\text{ and } x.RightMoves = \\varnothing$$$

Lean4

theorem isEmpty (x : PGame) [IsEmpty x.LeftMoves] [IsEmpty x.RightMoves] : x ≈ 0 :=
  (Relabelling.isEmpty x).equiv

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

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

Разделы

Аффилиация

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