exists_isNIndepSet_indepNum

Mathlib.Combinatorics.SimpleGraph.Clique

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

← MathLib Explorer

English

In a finite graph there exists an n-independent set of size equal to indepNum(G).

Русский

В конечном графе существует n-независимое множество размером, равным indepNum(G).

LaTeX

$$$\\exists s, G.IsNIndepSet G.indepNum s$$$

Lean4

theorem exists_isNIndepSet_indepNum [Finite α] : ∃ s, G.IsNIndepSet G.indepNum s :=
  by
  simp_rw [indepNum, ← isNClique_compl]
  exact exists_isNClique_cliqueNum

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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