cliqueSet_zero

Mathlib.Combinatorics.SimpleGraph.Clique

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

English

The zero cliqueSet corresponds to trivial singletons and empty graph structure.

Русский

Нулевая клика задаёт тривиальные множества вершин и пустые графы.

LaTeX

$$For any graph $G$, $G.cliqueSet(0)=\{\emptyset\}$.$$

Lean4

@[simp]
theorem cliqueSet_zero (G : SimpleGraph α) : G.cliqueSet 0 = {∅} :=
  Set.ext fun s => by simp

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

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

Разделы

Аффилиация

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