CliqueFreeOn — Mathlib

English

CliqueFreeOn G s n means that there are no n-cliques contained entirely in the subset s of vertices of G.

Русский

CliqueFreeOn G s n означает, что в подмножестве вершин s графа G нет клики размера n.

LaTeX

$$Definition: $G$ is a simple graph, $s$ is a subset of vertices, and $n$ a natural number; $G$ is $n$-clique-free on $s$ if for every $t$ with $t\subseteq s$, $G$ has no $n$-clique on $t$.$$

Lean4

/-- `G.CliqueFreeOn s n` means that `G` has no `n`-cliques contained in `s`. -/
def CliqueFreeOn (G : SimpleGraph α) (s : Set α) (n : ℕ) : Prop :=
  ∀ ⦃t⦄, ↑t ⊆ s → ¬G.IsNClique n t

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