isMaximalIndepSet — Mathlib

English

From a maximum independent set, derive a maximal independent set.

Русский

Из максимального независимого множества получаем максимальное независимое множество.

LaTeX

$$From a maximum independent set M, infer that it is a maximal independent set.$$

Lean4

theorem isMaximalIndepSet [Fintype α] (s : Finset α) (M : G.IsMaximumIndepSet s) : Maximal G.IsIndepSet s :=
  by
  rw [← isMaximalClique_compl]
  rw [← isMaximumClique_compl] at M
  exact IsMaximumClique.isMaximalClique s M

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