mem_incidenceSet

Mathlib.Combinatorics.SimpleGraph.Basic

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

English

For vertices v,w, the edge s(v,w) is in incidenceSet(v) exactly when v is adjacent to w.

Русский

Для вершин v,w ребро s(v,w) принадлежит inc(v) тогда и только тогда, когда v смежна с w.

LaTeX

$$$s(v,w) \\in G.incidenceSet(v) \\iff G.Adj(v,w)$$$

Lean4

@[simp]
theorem mem_incidenceSet (v w : V) : s(v, w) ∈ G.incidenceSet v ↔ G.Adj v w := by simp [incidenceSet]

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

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

Разделы

Аффилиация

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