mem_incidence_iff_neighbor

Mathlib.Combinatorics.SimpleGraph.Basic

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

English

Edge s(v,w) belongs to incidenceSet(v) if and only if w is a neighbor of v.

Русский

Ребро s(v,w) принадлежит inc(v) тогда и только тогда, когда w — сосед v.

LaTeX

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

Lean4

theorem mem_incidence_iff_neighbor {v w : V} : s(v, w) ∈ G.incidenceSet v ↔ w ∈ G.neighborSet v := by
  simp only [mem_incidenceSet, mem_neighborSet]

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

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

Разделы

Аффилиация

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