indepNum_compl

Mathlib.Combinatorics.SimpleGraph.Clique

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

English

The indepNum of the complement equals the cliqueNum of the original graph.

Русский

IndepNum дополнения равно CliqueNum исходного графа.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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