mem_left

Mathlib.SetTheory.Game.Domineering

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

← MathLib Explorer

English

x ≤ birthday(x).toGame for any game x.

Русский

Для любого x выполняется x ≤ (birthday(x)).toGame.

LaTeX

$$$x \le (x.birthday).toGame$$$

Lean4

theorem mem_left {b : Board} (x : ℤ × ℤ) : x ∈ left b ↔ x ∈ b ∧ (x.1, x.2 - 1) ∈ b :=
  Finset.mem_inter.trans (and_congr Iff.rfl Finset.mem_map_equiv)

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

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

Разделы

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

Аффилиация

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