isMaximalIndepSet_compl — Mathlib

English

Maximal G^c.IsIndepSet s iff Maximal G.IsClique s.

Русский

Максимальное в дополнении графа независимое множество эквивалентно максимальной клике в исходном графе.

LaTeX

$$Maximal (G^c).IsIndepSet s ↔ Maximal G.IsClique s$$

Lean4

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

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