CliqueFree — Mathlib

English

CliqueFree(n) means that the graph has no n-cliques; i.e., no subset of vertices of size n forms a clique.

Русский

CliqueFree(n) означает, что у графа нет n-клик; то есть ни одна подмножество вершин размера n не образует клику.

LaTeX

$$$ G.CliqueFree(n) \equiv \forall t, \neg G.IsNClique(n,t). $$$

Lean4

/-- `G.CliqueFree n` means that `G` has no `n`-cliques. -/
def CliqueFree (n : ℕ) : Prop :=
  ∀ t, ¬G.IsNClique n t

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