isNIndepSet_compl — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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