isMaximumClique_compl — Mathlib

English

If t is a maximum independent set, then |t| equals indepNum(G).

Русский

Если t — максимальное независимое множество, то |t| = indepNum(G).

LaTeX

$$$\\text{If } t \\text{ is a maximum independent set, then } |t| = \\operatorname{indepNum}(G)$$$

Lean4

@[simp]
theorem isMaximumClique_compl [Fintype α] (s : Finset α) : Gᶜ.IsMaximumClique s ↔ G.IsMaximumIndepSet s := by
  simp [isMaximumIndepSet_iff, isMaximumClique_iff]

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