isNClique_compl — Mathlib

English

An n-clique in the complement graph corresponds to an n-independent set in the original graph.

Русский

N-клика в дополнении соответствует n-независимому множеству в исходном графе.

LaTeX

$$$G^{\\mathsf{c}}.IsNClique n s \\iff G.IsNIndepSet n s.$$$

Lean4

/-- An `n`-independent set is an `n`-clique in the complement graph and vice versa. -/
@[simp]
theorem isNClique_compl : Gᶜ.IsNClique n s ↔ G.IsNIndepSet n s :=
  by
  rw [isNIndepSet_iff]
  simp [isNClique_iff]

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