isNClique_empty

Mathlib.Combinatorics.SimpleGraph.Clique

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

English

An NClique of G on s is equivalent to G being a clique on s together with |s| = n.

Русский

NClique графа G на s эквивалентно тому, что G является кликой на s и |s| = n.

LaTeX

$$$$ G.IsNClique n s \\iff (G.IsClique\\ s) \\land \\#s = n $$$$

Lean4

@[simp]
theorem isNClique_empty : G.IsNClique n ∅ ↔ n = 0 := by simp [isNClique_iff, eq_comm]

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

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

Разделы

Аффилиация

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