card_of_mem_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem card_of_mem_left {b : Board} {m : ℤ × ℤ} (h : m ∈ left b) : 2 ≤ Finset.card b :=
  by
  have w₁ : m ∈ b := (Finset.mem_inter.1 h).1
  have w₂ : (m.1, m.2 - 1) ∈ b.erase m := snd_pred_mem_erase_of_mem_left 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₁

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