right

Mathlib.SetTheory.Game.Domineering

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

English

m ∈ left(b) iff m ∈ b and (m1, m2-1) ∈ b.

Русский

m принадлежит left(b) тогда и только тогда, когда m ∈ b и (m1, m2-1) ∈ b.

LaTeX

$$$m \in \mathrm{left}(b) \iff m \in b \land (m_1, m_2-1) \in b$$$

Lean4

/-- Right can play anywhere that a square and the square to the left are open. -/
def right (b : Board) : Finset (ℤ × ℤ) :=
  b ∩ b.map shiftRight

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

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

Разделы

Аффилиация

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