# Trails and Eulerian trails #

This module contains additional theory about trails, including Eulerian trails (also known as Eulerian circuits).

## Tags #

Eulerian trails

@[reducible, inline]
abbrev SimpleGraph.Walk.IsTrail.edgesFinset {V : Type u_1} {G : } {u : V} {v : V} {p : G.Walk u v} (h : p.IsTrail) :

The edges of a trail as a finset, since each edge in a trail appears exactly once.

Equations
• h.edgesFinset = { val := p.edges, nodup := }
Instances For
theorem SimpleGraph.Walk.IsTrail.even_countP_edges_iff {V : Type u_1} {G : } [] {u : V} {v : V} {p : G.Walk u v} (ht : p.IsTrail) (x : V) :
Even (List.countP (fun (e : Sym2 V) => decide (x e)) p.edges) u vx u x v
def SimpleGraph.Walk.IsEulerian {V : Type u_1} {G : } [] {u : V} {v : V} (p : G.Walk u v) :

An Eulerian trail (also known as an "Eulerian path") is a walk p that visits every edge exactly once. The lemma SimpleGraph.Walk.IsEulerian.IsTrail shows that these are trails.

Combine with p.IsCircuit to get an Eulerian circuit (also known as an "Eulerian cycle").

Equations
• p.IsEulerian = eG.edgeSet, List.count e p.edges = 1
Instances For
theorem SimpleGraph.Walk.IsEulerian.isTrail {V : Type u_1} {G : } [] {u : V} {v : V} {p : G.Walk u v} (h : p.IsEulerian) :
p.IsTrail
theorem SimpleGraph.Walk.IsEulerian.mem_edges_iff {V : Type u_1} {G : } [] {u : V} {v : V} {p : G.Walk u v} (h : p.IsEulerian) {e : Sym2 V} :
e p.edges e G.edgeSet
def SimpleGraph.Walk.IsEulerian.fintypeEdgeSet {V : Type u_1} {G : } [] {u : V} {v : V} {p : G.Walk u v} (h : p.IsEulerian) :
Fintype G.edgeSet

The edge set of an Eulerian graph is finite.

Equations
Instances For
theorem SimpleGraph.Walk.IsTrail.isEulerian_of_forall_mem {V : Type u_1} {G : } [] {u : V} {v : V} {p : G.Walk u v} (h : p.IsTrail) (hc : eG.edgeSet, e p.edges) :
p.IsEulerian
theorem SimpleGraph.Walk.isEulerian_iff {V : Type u_1} {G : } [] {u : V} {v : V} (p : G.Walk u v) :
p.IsEulerian p.IsTrail eG.edgeSet, e p.edges
theorem SimpleGraph.Walk.IsEulerian.edgesFinset_eq {V : Type u_1} {G : } [] [Fintype G.edgeSet] {u : V} {v : V} {p : G.Walk u v} (h : p.IsEulerian) :
.edgesFinset = G.edgeFinset
theorem SimpleGraph.Walk.IsEulerian.even_degree_iff {V : Type u_1} {G : } [] {x : V} {u : V} {v : V} {p : G.Walk u v} (ht : p.IsEulerian) [] [DecidableRel G.Adj] :
Even (G.degree x) u vx u x v
theorem SimpleGraph.Walk.IsEulerian.card_filter_odd_degree {V : Type u_1} {G : } [] [] [DecidableRel G.Adj] {u : V} {v : V} {p : G.Walk u v} (ht : p.IsEulerian) {s : } (h : s = Finset.filter (fun (v : V) => Odd (G.degree v)) Finset.univ) :
s.card = 0 s.card = 2
theorem SimpleGraph.Walk.IsEulerian.card_odd_degree {V : Type u_1} {G : } [] [] [DecidableRel G.Adj] {u : V} {v : V} {p : G.Walk u v} (ht : p.IsEulerian) :
Fintype.card {v : V | Odd (G.degree v)} = 0 Fintype.card {v : V | Odd (G.degree v)} = 2