incidenceSetFintype — Mathlib

English

There is a finite-type structure on the incidence set at v, via a bijection with the neighbor set.

Русский

Для IncidenceSet на вершине v существует конечная структура, полученная через биекцию с множством соседей.

LaTeX

$$Fintype (G.incidenceSet v) is defined via an equivalence with (G.neighborSet v).$$

Lean4

instance incidenceSetFintype [DecidableEq V] : Fintype (G.incidenceSet v) :=
  Fintype.ofEquiv (G.neighborSet v) (G.incidenceSetEquivNeighborSet v).symm

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