cliqueSet_one

Mathlib.Combinatorics.SimpleGraph.Clique

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

English

CliqueSet(1) is the range of the singleton operation.

Русский

CliqueSet(1) равен диапазону операции взятия единичного множества.

LaTeX

$$For any graph $G$, $G.cliqueSet(1) = \operatorname{Set.range}(\text{singleton})$.$$

Lean4

@[simp]
theorem cliqueSet_one (G : SimpleGraph α) : G.cliqueSet 1 = Set.range singleton :=
  Set.ext fun s => by simp [eq_comm]

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

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

Разделы

Аффилиация

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