isClique_bot_iff

Mathlib.Combinatorics.SimpleGraph.Clique

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

English

For the bottom graph, G.IsClique s holds iff s is subsingleton.

Русский

Для нулевого графа утверждение G.IsClique s эквивалентно тому, что s является подселентной (subsingleton).

LaTeX

$$$ (\perp : SimpleGraph\ α).IsClique s \iff (s : Set α).Subsingleton $$$

Lean4

@[simp]
theorem isClique_bot_iff : (⊥ : SimpleGraph α).IsClique s ↔ (s : Set α).Subsingleton :=
  Set.pairwise_bot_iff

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

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

Разделы

Аффилиация

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