isClique_universalVerts

Mathlib.Combinatorics.SimpleGraph.UniversalVerts

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

English

The set of universal vertices forms a clique.

Русский

Множество универсальных вершин образует клику.

LaTeX

$$G.IsClique G.universalVerts$$

Lean4

theorem isClique_universalVerts (G : SimpleGraph V) : G.IsClique G.universalVerts := fun _ _ _ hy hxy ↦ hy hxy.symm

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

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

Разделы

Аффилиация

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