indepNum — Mathlib

English

The indepNum of G is the maximal possible size of an independent set of G.

Русский

indepNum графа G — максимальная возможная величина размера независимого множества графа.

LaTeX

$$$\\operatorname{indepNum}(G) = \\sup\\{\, n \\in \\mathbb{N} \\mid \\exists s, G.IsNIndepSet(n,s) \\}$$$

Lean4

/-- The maximal number of vertices of an independent set in a graph `G`. -/
noncomputable def indepNum (G : SimpleGraph α) : ℕ :=
  sSup {n | ∃ s, G.IsNIndepSet n s}

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