moveLeft

Mathlib.SetTheory.Game.Domineering

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

← MathLib Explorer

English

moveLeft(b, m) is the board with m and (m1, m2-1) removed.

Русский

moveLeft(b, m) — это доска, у которой удалены m и (m1, m2-1).

LaTeX

$$$\text{moveLeft}(b, m) = (b \setminus \{m\}) \setminus \{(m_1, m_2-1)\}$$$

Lean4

/-- After Left moves, two vertically adjacent squares are removed from the board. -/
def moveLeft (b : Board) (m : ℤ × ℤ) : Board :=
  (b.erase m).erase (m.1, m.2 - 1)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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