edgeSet

Mathlib.Combinatorics.SimpleGraph.Walk

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Walk.edgeSet

English

The edgeSet of a walk is the set of its edges.

Русский

EdgeSet хода — множество его рёбер.

LaTeX

$$$ \text{edgeSet}(p) = \{ e \in \mathrm{Sym}^2(V) \mid e \in p.edges \} $$$

Lean4

/-- The `Set` of edges of a walk. -/
def edgeSet {u v : V} (p : G.Walk u v) : Set (Sym2 V) :=
  {e | e ∈ p.edges}

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

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

Разделы

Аффилиация

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