coe_edgeFinset

Mathlib.Combinatorics.SimpleGraph.Finite

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

English

The edgeFinset of a graph, viewed as a set, coincides with the underlying edge set.

Русский

edgeFinset графа трактуется как обычное множество ребер графа.

LaTeX

$$$(G.edgeFinset : \\mathrm{Set}(\\mathrm{Sym}^2 V)) = G.edgeSet$$$

Lean4

@[norm_cast]
theorem coe_edgeFinset : (G.edgeFinset : Set (Sym2 V)) = G.edgeSet :=
  Set.coe_toFinset _

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

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

Разделы

Аффилиация

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