cliqueNum — Mathlib

English

Let G be a graph. The clique number ω(G) is the largest size of a clique contained in G; equivalently, ω(G) = sup { n ∈ ℕ | ∃ s : Finset α, G.IsNClique n s }.

Русский

Пусть G — граф. Кликовое число ω(G) — наибольшая мощность клики графа; эквивалентно ω(G) = sup { n ∈ ℕ | ∃ s : Finset α, G.IsNClique n s }.

LaTeX

$$$\\operatorname{cliqueNum}(G) = \\sup \\{ n \\in \\mathbb{N} \\mid \\exists s : Finset \\alpha,\\ G.IsNClique n s \\}$$$

Lean4

/-- The maximum number of vertices in a clique of a graph `G`. -/
noncomputable def cliqueNum (G : SimpleGraph α) : ℕ :=
  sSup {n | ∃ s, G.IsNClique n s}

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