mem_neighborSet

Mathlib.Combinatorics.SimpleGraph.Basic

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

English

For all v,w, w is a neighbor of v iff v and w are adjacent.

Русский

Для всех v,w верно: w является соседом v тогда и только тогда, когда v и w смежны.

LaTeX

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

Lean4

@[simp]
theorem mem_neighborSet (v w : V) : w ∈ G.neighborSet v ↔ G.Adj v w :=
  Iff.rfl

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

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

Разделы

Аффилиация

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