incidenceFinset

Mathlib.Combinatorics.SimpleGraph.Finite

URI: https://scilib.ai/kg/mathlib#SimpleGraph.incidenceFinset

English

The finite version of the incidence set is obtained by taking the toFinset image of the incidenceSet.

Русский

Финсет-версия incidenceSet получается как образ через toFinset.

LaTeX

$$$ (G.incidenceSet v).toFinset $$$

Lean4

/-- This is the `Finset` version of `incidenceSet`. -/
def incidenceFinset [DecidableEq V] : Finset (Sym2 V) :=
  (G.incidenceSet v).toFinset

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

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

Разделы

Аффилиация

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