adj_comm

Mathlib.Combinatorics.SimpleGraph.Subgraph

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Subgraph.adj_comm

English

Adjacency in a subgraph is symmetric: H.Adj u v if and only if H.Adj v u.

Русский

Симметричность смежности в подграфе: H.Adj u v ⇔ H.Adj v u.

LaTeX

$$$H.Adj\,u\,v \;\Leftrightarrow\; H.Adj\,v\,u$$$

Lean4

theorem adj_comm (G' : Subgraph G) (v w : V) : G'.Adj v w ↔ G'.Adj w v :=
  ⟨fun x ↦ G'.symm x, fun x ↦ G'.symm x⟩

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

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

Разделы

Аффилиация

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