moveRight_smaller — Mathlib

English

For any right move m, the half-cardinality strictly decreases: card(moveRight(b,m))/2 < card(b)/2.

Русский

Для любого правого хода m половинная кардинальность строго уменьшается: card(moveRight(b,m))/2 < card(b)/2.

LaTeX

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

Lean4

theorem moveRight_smaller {b : Board} {m : ℤ × ℤ} (h : m ∈ right b) :
    Finset.card (moveRight b m) / 2 < Finset.card b / 2 := by simp [← moveRight_card h]

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