snd_pred_mem_erase_of_mem_left

Mathlib.SetTheory.Game.Domineering

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

← MathLib Explorer

English

If h ∈ left(b), then (m1, m2-1) ∈ b.erase m.

Русский

Если h ∈ left(b), тогда (m1, m2-1) ∈ b.erase m.

LaTeX

$$$(m_1, m_2-1) \in b \setminus \{m\}$$$

Lean4

theorem snd_pred_mem_erase_of_mem_left {b : Board} {m : ℤ × ℤ} (h : m ∈ left b) : (m.1, m.2 - 1) ∈ b.erase m :=
  by
  rw [mem_left] at h
  apply Finset.mem_erase_of_ne_of_mem _ h.2
  exact ne_of_apply_ne Prod.snd (pred_ne_self m.2)

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

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

Разделы

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

Аффилиация

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