mathlib3 documentation

combinatorics.simple_graph.trails

Trails and Eulerian trails #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

Todo #

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 v x 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} :

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 simple_graph.edge_set G e 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) :
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 v x 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