isClique_pair

Mathlib.Combinatorics.SimpleGraph.Clique

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

English

For any two vertices a,b, the set {a,b} is a clique iff a ≠ b implies G.Adj a b.

Русский

Для любых вершин a,b множество {a,b} является кликой тогда и только тогда, когда a ≠ b предполагает G.Adj a b.

LaTeX

$$$ G.IsClique \{a, b\} \iff a \neq b \rightarrow G.Adj a b $$$

Lean4

theorem isClique_pair : G.IsClique { a, b } ↔ a ≠ b → G.Adj a b :=
  Set.pairwise_pair_of_symmetric G.symm

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

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

Разделы

Аффилиация

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