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 #
simple_graph.walk.is_eulerianis the predicate that a trail is an Eulerian trail.simple_graph.walk.is_trail.even_countp_edges_iffgives 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_iffgives a condition on the degrees of vertices when there exists an Eulerian trail.simple_graph.walk.is_eulerian.card_odd_degreegives 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_degreeholds.
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.
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) :
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
- p.is_eulerian = ∀ (e : sym2 V), e ∈ ⇑simple_graph.edge_set G → list.count e p.edges = 1
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) :
p.is_trail
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 ∈ ⇑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.edges_finset_eq
{V : Type u_1}
{G : simple_graph V}
[decidable_eq V]
[fintype ↥(⇑simple_graph.edge_set G)]
{u v : V}
{p : G.walk u v}
(h : p.is_eulerian) :
_.edges_finset = G.edge_finset
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] :
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) :
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) :