cliqueNum_compl

Mathlib.Combinatorics.SimpleGraph.Clique

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

English

The clique number of the complement equals the independence number of the graph.

Русский

Клика-число дополнения графа равно числу независимости графа.

LaTeX

$$$\\operatorname{cliqueNum}(G^c) = \\operatorname{indepNum}(G)$$$

Lean4

@[simp]
theorem cliqueNum_compl : Gᶜ.cliqueNum = G.indepNum := by simp [indepNum, cliqueNum]

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

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

Разделы

Аффилиация

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