cliqueSet_mono

Mathlib.Combinatorics.SimpleGraph.Clique

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

English

The clique-set equality with empty set is equivalent to clique-freeness framing.

Русский

Равенство множества кликов пустому эквивалентно формулировке клик-фри.

LaTeX

$$For all graphs $G$ and $n$, $G.cliqueSet(n)=\emptyset$ iff $G.CliqueFree n$.$$

Lean4

@[gcongr, mono]
theorem cliqueSet_mono (h : G ≤ H) : G.cliqueSet n ⊆ H.cliqueSet n := fun _ ↦ IsNClique.mono h

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

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

Разделы

Аффилиация

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