neighborSet — Mathlib

English

The neighbor set of a vertex v in a subgraph G' is the set of all vertices w such that G'.Adj(v,w) holds.

Русский

Множество соседей вершины v в подграфе G' состоит из всех вершин w, для которых выполняется G'.Adj(v,w).

LaTeX

$$$\\mathrm{neighborSet}(G')(v) = \\{ w \\in V \\mid G'.Adj(v,w) \\}$$$

Lean4

/-- `G'.neighborSet v` is the set of vertices adjacent to `v` in `G'`. -/
def neighborSet (G' : Subgraph G) (v : V) : Set V :=
  {w | G'.Adj v w}

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