moveLeft_smaller — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem moveLeft_smaller {b : Board} {m : ℤ × ℤ} (h : m ∈ left b) :
    Finset.card (moveLeft b m) / 2 < Finset.card b / 2 := by simp [← moveLeft_card h]

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