card_of_mem_right — Mathlib

English

If m ∈ right(b), then 2 ≤ card b.

Русский

Если m ∈ right(b), то 2 ≤ кардиналность b.

LaTeX

$$$2 \le |b|$$$

Lean4

theorem card_of_mem_right {b : Board} {m : ℤ × ℤ} (h : m ∈ right b) : 2 ≤ Finset.card b :=
  by
  have w₁ : m ∈ b := (Finset.mem_inter.1 h).1
  have w₂ := fst_pred_mem_erase_of_mem_right h
  have i₁ := Finset.card_erase_lt_of_mem w₁
  have i₂ := Nat.lt_of_le_of_lt (Nat.zero_le _) (Finset.card_erase_lt_of_mem w₂)
  exact Nat.lt_of_le_of_lt i₂ i₁

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