edgeFinset — Mathlib

English

The edgeFinset of a graph is the finite set of its edges, viewed as finite sets of vertex-pairs.

Русский

edgeFinset графа — конечно множество его ребер, рассматриваемое как конечные пары вершин.

LaTeX

$$$\\mathrm{edgeFinset} := \\mathrm{Set.toFinset}(\\mathrm{G}.\\mathrm{edgeSet}).$$$

Lean4

/-- The `edgeSet` of the graph as a `Finset`. -/
abbrev edgeFinset : Finset (Sym2 V) :=
  Set.toFinset G.edgeSet

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