isClique_compl — Mathlib

English

A set is a clique in the complement graph if and only if it is an independent set in the original graph.

Русский

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

LaTeX

$$$G^{\\mathsf{c}}.IsClique\ \(s)\\iff G.IsIndepSet(s).$$$

Lean4

/-- An independent set is a clique in the complement graph and vice versa. -/
@[simp]
theorem isClique_compl : Gᶜ.IsClique s ↔ G.IsIndepSet s :=
  by
  rw [isIndepSet_iff, isClique_iff]; repeat rw [Set.Pairwise]
  simp_all [compl_adj]

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