left — Mathlib

English

Left can play exactly on those squares where a square and the one below it are both open.

Русский

Левый игрок может ходить только в тех клетках, где клетка и клетка ниже открыты.

LaTeX

$$$\operatorname{left}(b) = \{(i,j)\in \mathbb{Z}^2 : (i,j)\in b \text{ и } (i,j-1)\in b\}$$$

Lean4

/-- Left can play anywhere that a square and the square below it are open. -/
def left (b : Board) : Finset (ℤ × ℤ) :=
  b ∩ b.map shiftUp

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