indepSetFinset

Mathlib.Combinatorics.SimpleGraph.Clique

URI: https://scilib.ai/kg/mathlib#SimpleGraph.indepSetFinset

English

The n-independent sets can be collected into a finite set of Finset α.

Русский

Независимые множества размера n образуют конечный набор множин Finset α.

LaTeX

$$$\\mathrm{indepSetFinset}(n) :\\ Finset(\\mathrm{Finset}\\;\\alpha)$$$

Lean4

/-- The `n`-independent sets in a graph as a finset. -/
def indepSetFinset (n : ℕ) : Finset (Finset α) :=
  {s | G.IsNIndepSet n s}

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru