card_le_indepNum — Mathlib

English

If t is an independent set in a finite graph, then |t| ≤ indepNum(G).

Русский

Если t—независимое множество в конечном графе, то |t| ≤ indepNum(G).

LaTeX

$$$\\forall t,\\ G.IsIndepSet(t) \\Rightarrow \\#t \\le \\operatorname{indepNum}(G)$$$

Lean4

theorem card_le_indepNum [Finite α] {t : Finset α} (tc : G.IsIndepSet t) : #t ≤ G.indepNum :=
  by
  cases nonempty_fintype α
  rw [← isClique_compl] at tc
  simp_rw [indepNum, ← isNClique_compl]
  exact tc.card_le_cliqueNum

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