moveLeft_card — Mathlib

English

If m is a legal left move in b, then the number of legal moves after performing that move satisfies |moveLeft(b, m)| = |b| − 2.

Русский

Пусть m является допустимым левым ходом на доске b. Тогда число допустимых ходов после выполнения этого хода равно числу ходов на доске b минус 2.

LaTeX

$$$m \in \mathrm{left}(b) \Rightarrow |\mathrm{moveLeft}(b,m)| + 2 = |b|$$$

Lean4

theorem moveLeft_card {b : Board} {m : ℤ × ℤ} (h : m ∈ left b) : Finset.card (moveLeft b m) + 2 = Finset.card b :=
  by
  dsimp only [moveLeft]
  rw [Finset.card_erase_of_mem (snd_pred_mem_erase_of_mem_left h)]
  rw [Finset.card_erase_of_mem (Finset.mem_of_mem_inter_left h)]
  exact tsub_add_cancel_of_le (card_of_mem_left h)

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