edgesFinset_eq

Mathlib.Combinatorics.SimpleGraph.Trails

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

← MathLib Explorer

English

For an Eulerian walk p, the finite edges set equals the trail's edges Finset.

Русский

Для эйлерова пути p конечное множество рёбер совпадает с Finset его рёбер.

LaTeX

$$h.isTrail.edgesFinset = G.edgeFinset$$

Lean4

theorem edgesFinset_eq [Fintype G.edgeSet] {u v : V} {p : G.Walk u v} (h : p.IsEulerian) :
    h.isTrail.edgesFinset = G.edgeFinset := by
  ext e
  simp [h.mem_edges_iff]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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