maximumIndepSet_card_eq_indepNum — Mathlib

English

There exists a maximum independent set in any finite graph.

Русский

В любом конечном графе существует максимальное независимое множество.

LaTeX

$$Exists s, G.IsMaximumIndepSet s$$

Lean4

theorem maximumIndepSet_card_eq_indepNum [Fintype α] (t : Finset α) (tmc : G.IsMaximumIndepSet t) : #t = G.indepNum :=
  by
  rw [← isMaximumClique_compl] at tmc
  simp_rw [indepNum, ← isNClique_compl]
  exact Gᶜ.maximumClique_card_eq_cliqueNum t tmc

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