commonNeighbors — Mathlib

English

The set of common neighbors of v and w is the intersection of their neighbor sets.

Русский

Множество общих соседей вершин v и w есть пересечение их множеств соседей.

LaTeX

$$$G.commonNeighbors(v,w) = G.neighborSet(v) \\cap G.neighborSet(w)$$$

Lean4

/-- The set of common neighbors between two vertices `v` and `w` in a graph `G` is the
intersection of the neighbor sets of `v` and `w`. -/
def commonNeighbors (v w : V) : Set V :=
  G.neighborSet v ∩ G.neighborSet w

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