fintypeEdgeSet — Mathlib

English

The edge set of an Eulerian walk is finite.

Русский

Множество рёбер эйлерова следа является конечным.

LaTeX

$$$ p.IsEulerian \Rightarrow Fintype(G.edgeSet.Elem) $$$

Lean4

/-- The edge set of an Eulerian graph is finite. -/
def fintypeEdgeSet {u v : V} {p : G.Walk u v} (h : p.IsEulerian) : Fintype G.edgeSet :=
  Fintype.ofFinset h.isTrail.edgesFinset fun e => by simp only [Finset.mem_mk, Multiset.mem_coe, h.mem_edges_iff]

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