moveRight_card — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem moveRight_card {b : Board} {m : ℤ × ℤ} (h : m ∈ right b) : Finset.card (moveRight b m) + 2 = Finset.card b :=
  by
  dsimp only [moveRight]
  rw [Finset.card_erase_of_mem (fst_pred_mem_erase_of_mem_right h)]
  rw [Finset.card_erase_of_mem (Finset.mem_of_mem_inter_left h)]
  exact tsub_add_cancel_of_le (card_of_mem_right h)

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