mem_neighborSet

Mathlib.Combinatorics.SimpleGraph.Subgraph

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

English

For any G', v, and w, w is a member of G'.neighborSet(v) if and only if G'.Adj(v,w).

Русский

Для подграфа G', вершины v и w: w принадлежит G'.neighborSet(v) тогда и только тогда, когда G'.Adj(v,w).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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