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}