isMaximalClique_compl — Mathlib

English

The complement graph has a maximum clique exactly when the original graph has a maximum independent set.

Русский

У комплементарного графа максимальная клика соответствует максимальному независимому множеству исходного графа.

LaTeX

$$IsMaximumClique(G^c, s) ↔ IsMaximumIndepSet(G, s)$$

Lean4

@[simp]
theorem isMaximalClique_compl (s : Finset α) : Maximal Gᶜ.IsClique s ↔ Maximal G.IsIndepSet s := by
  simp [isMaximalIndepSet_iff, isMaximalClique_iff]

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