neighborFinset — Mathlib

English

For a graph G on V and a vertex v, the neighborFinset v is the Finset of all neighbors of v.

Русский

Для графа G на множестве вершин V и вершины v множества соседей v есть Finset соседей вершины v.

LaTeX

$$$ G.neighborFinset v = (G.neighborSet v).toFinset $$$

Lean4

/-- `G.neighborFinset v` is the `Finset` version of `G.neighborSet v` in case `G` is
locally finite at `v`. -/
def neighborFinset : Finset V :=
  (G.neighborSet v).toFinset

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