cliqueFinset — Mathlib

English

The n-cliques of G form a Finset of Finsets; i.e., a finite collection of vertex-sets that are cliques of size n.

Русский

Графовые n-клики образуют множество Finset над Finset α; иными словами, конечная совокупность подмножеств вершин, образующих клику размера n.

LaTeX

$$$\\mathrm{cliqueFinset}(n) = \\{ s : Finset(\\alpha) \\mid G.IsNClique n\\, s \\}.$$$

Lean4

/-- The `n`-cliques in a graph as a finset. -/
def cliqueFinset (n : ℕ) : Finset (Finset α) :=
  {s | G.IsNClique n s}

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