cliqueSet_eq_empty_iff — Mathlib

English

The clique set is empty iff the graph is not containing any n-clique at all.

Русский

Множество кликов пусто тогда и только тогда, когда граф не содержит вовсе ни одной n‑клики.

LaTeX

$$For all graphs $G$ and $n$, $G.cliqueSet(n)=\emptyset$ iff $G.CliqueFree n$.$$

Lean4

@[simp]
theorem cliqueSet_eq_empty_iff : G.cliqueSet n = ∅ ↔ G.CliqueFree n := by
  simp_rw [CliqueFree, Set.eq_empty_iff_forall_notMem, mem_cliqueSet_iff]

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