fst_pred_mem_erase_of_mem_right

Mathlib.SetTheory.Game.Domineering

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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