card_parts_le — Mathlib

English

The number of parts in the finpartition is at most r.

Русский

Число частей финразбиения не превосходит r.

LaTeX

$$$\#h.finpartition.parts \le r.$$$

Lean4

theorem card_parts_le [DecidableEq V] : #h.finpartition.parts ≤ r :=
  by
  by_contra! l
  obtain ⟨z, -, hz⟩ := h.finpartition.exists_subset_part_bijOn
  have ncf : ¬G.CliqueFree #z :=
    by
    refine IsNClique.not_cliqueFree ⟨fun v hv w hw hn ↦ ?_, rfl⟩
    contrapose! hn
    exact hz.injOn hv hw (by rwa [← h.not_adj_iff_part_eq])
  rw [Finset.card_eq_of_equiv hz.equiv] at ncf
  exact absurd (h.1.mono (Nat.succ_le_of_lt l)) ncf

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