# mathlibdocumentation

combinatorics.simple_graph.trails

# Trails and Eulerian trails #

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

## Main definitions #

• simple_graph.walk.is_eulerian is the predicate that a trail is an Eulerian trail.
• simple_graph.walk.is_trail.even_countp_edges_iff gives a condition on the number of edges in a trail that can be incident to a given vertex.
• simple_graph.walk.is_eulerian.even_degree_iff gives a condition on the degrees of vertices when there exists an Eulerian trail.
• simple_graph.walk.is_eulerian.card_odd_degree gives the possible numbers of odd-degree vertices when there exists an Eulerian trail.

## Todo #

• Prove that there exists an Eulerian trail when the conclusion to simple_graph.walk.is_eulerian.card_odd_degree holds.

## Tags #

Eulerian trails

@[reducible]
def simple_graph.walk.is_trail.edges_finset {V : Type u_1} {G : simple_graph V} {u v : V} {p : G.walk u v} (h : p.is_trail) :

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

Equations
theorem simple_graph.walk.is_trail.even_countp_edges_iff {V : Type u_1} {G : simple_graph V} [decidable_eq V] {u v : V} {p : G.walk u v} (ht : p.is_trail) (x : V) :
even (list.countp (λ (e : sym2 V), x e) p.edges) u vx u x v
def simple_graph.walk.is_eulerian {V : Type u_1} {G : simple_graph V} [decidable_eq V] {u v : V} (p : G.walk u v) :
Prop

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

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

Equations
theorem simple_graph.walk.is_eulerian.is_trail {V : Type u_1} {G : simple_graph V} [decidable_eq V] {u v : V} {p : G.walk u v} (h : p.is_eulerian) :
theorem simple_graph.walk.is_eulerian.mem_edges_iff {V : Type u_1} {G : simple_graph V} [decidable_eq V] {u v : V} {p : G.walk u v} (h : p.is_eulerian) {e : sym2 V} :
def simple_graph.walk.is_eulerian.fintype_edge_set {V : Type u_1} {G : simple_graph V} [decidable_eq V] {u v : V} {p : G.walk u v} (h : p.is_eulerian) :

The edge set of an Eulerian graph is finite.

Equations
theorem simple_graph.walk.is_trail.is_eulerian_of_forall_mem {V : Type u_1} {G : simple_graph V} [decidable_eq V] {u v : V} {p : G.walk u v} (h : p.is_trail) (hc : ∀ (e : sym2 V), e G.edge_sete p.edges) :
theorem simple_graph.walk.is_eulerian_iff {V : Type u_1} {G : simple_graph V} [decidable_eq V] {u v : V} (p : G.walk u v) :
p.is_eulerian p.is_trail ∀ (e : sym2 V), e G.edge_sete p.edges
theorem simple_graph.walk.is_eulerian.edges_finset_eq {V : Type u_1} {G : simple_graph V} [decidable_eq V] [fintype (G.edge_set)] {u v : V} {p : G.walk u v} (h : p.is_eulerian) :
theorem simple_graph.walk.is_eulerian.even_degree_iff {V : Type u_1} {G : simple_graph V} [decidable_eq V] {x u v : V} {p : G.walk u v} (ht : p.is_eulerian) [fintype V] [decidable_rel G.adj] :
even (G.degree x) u vx u x v
theorem simple_graph.walk.is_eulerian.card_filter_odd_degree {V : Type u_1} {G : simple_graph V} [decidable_eq V] [fintype V] [decidable_rel G.adj] {u v : V} {p : G.walk u v} (ht : p.is_eulerian) {s : finset V} (h : s = finset.filter (λ (v : V), odd (G.degree v)) finset.univ) :
s.card = 0 s.card = 2
theorem simple_graph.walk.is_eulerian.card_odd_degree {V : Type u_1} {G : simple_graph V} [decidable_eq V] [fintype V] [decidable_rel G.adj] {u v : V} {p : G.walk u v} (ht : p.is_eulerian) :
fintype.card {v : V | odd (G.degree v)} = 0 fintype.card {v : V | odd (G.degree v)} = 2