Trails and Eulerian trails

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

Main definitions

• SimpleGraph.Walk.IsEulerian is the predicate that a trail is an Eulerian trail.
• SimpleGraph.Walk.IsTrail.even_countP_edges_iff gives a condition on the number of edges in a trail that can be incident to a given vertex.
• SimpleGraph.Walk.IsEulerian.even_degree_iff gives a condition on the degrees of vertices when there exists an Eulerian trail.
• SimpleGraph.Walk.IsEulerian.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 SimpleGraph.Walk.IsEulerian.card_odd_degree holds.

Tags

Eulerian trails

@[reducible]

def SimpleGraph.Walk.IsTrail.edgesFinset {V : Type u_1} {G : SimpleGraph V} {u : V} {v : V} {p : SimpleGraph.Walk G u v} (h : SimpleGraph.Walk.IsTrail p) : Finset (Sym2 V)

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

Equations

• SimpleGraph.Walk.IsTrail.edgesFinset h = { val := ↑(SimpleGraph.Walk.edges p), nodup := (_ : List.Nodup (SimpleGraph.Walk.edges p)) }

theorem SimpleGraph.Walk.IsTrail.even_countP_edges_iff {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {p : SimpleGraph.Walk G u v} (ht : SimpleGraph.Walk.IsTrail p) (x : V) : Even (List.countP (fun (e : Sym2 V) => decide (x ∈ e)) (SimpleGraph.Walk.edges p)) ↔ u ≠ v → x ≠ u ∧ x ≠ v

def SimpleGraph.Walk.IsEulerian {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : SimpleGraph.Walk G u v) : Prop

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

• SimpleGraph.Walk.IsEulerian p = ∀ e ∈ SimpleGraph.edgeSet G, List.count e (SimpleGraph.Walk.edges p) = 1

theorem SimpleGraph.Walk.IsEulerian.isTrail {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {p : SimpleGraph.Walk G u v} (h : SimpleGraph.Walk.IsEulerian p) : SimpleGraph.Walk.IsTrail p

theorem SimpleGraph.Walk.IsEulerian.mem_edges_iff {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {p : SimpleGraph.Walk G u v} (h : SimpleGraph.Walk.IsEulerian p) {e : Sym2 V} : e ∈ SimpleGraph.Walk.edges p ↔ e ∈ SimpleGraph.edgeSet G

def SimpleGraph.Walk.IsEulerian.fintypeEdgeSet {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {p : SimpleGraph.Walk G u v} (h : SimpleGraph.Walk.IsEulerian p) : Fintype ↑(SimpleGraph.edgeSet G)

The edge set of an Eulerian graph is finite.

Equations

• One or more equations did not get rendered due to their size.

theorem SimpleGraph.Walk.IsTrail.isEulerian_of_forall_mem {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {p : SimpleGraph.Walk G u v} (h : SimpleGraph.Walk.IsTrail p) (hc : ∀ e ∈ SimpleGraph.edgeSet G, e ∈ SimpleGraph.Walk.edges p) : SimpleGraph.Walk.IsEulerian p

theorem SimpleGraph.Walk.isEulerian_iff {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : SimpleGraph.Walk G u v) : SimpleGraph.Walk.IsEulerian p ↔ SimpleGraph.Walk.IsTrail p ∧ ∀ e ∈ SimpleGraph.edgeSet G, e ∈ SimpleGraph.Walk.edges p

theorem SimpleGraph.Walk.IsEulerian.edgesFinset_eq {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] [Fintype ↑(SimpleGraph.edgeSet G)] {u : V} {v : V} {p : SimpleGraph.Walk G u v} (h : SimpleGraph.Walk.IsEulerian p) : SimpleGraph.Walk.IsTrail.edgesFinset (_ : SimpleGraph.Walk.IsTrail p) = SimpleGraph.edgeFinset G

theorem SimpleGraph.Walk.IsEulerian.even_degree_iff {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {x : V} {u : V} {v : V} {p : SimpleGraph.Walk G u v} (ht : SimpleGraph.Walk.IsEulerian p) [Fintype V] [DecidableRel G.Adj] : Even (SimpleGraph.degree G x) ↔ u ≠ v → x ≠ u ∧ x ≠ v

theorem SimpleGraph.Walk.IsEulerian.card_filter_odd_degree {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] [Fintype V] [DecidableRel G.Adj] {u : V} {v : V} {p : SimpleGraph.Walk G u v} (ht : SimpleGraph.Walk.IsEulerian p) {s : Finset V} (h : s = Finset.filter (fun (v : V) => Odd (SimpleGraph.degree G v)) Finset.univ) : s.card = 0 ∨ s.card = 2

theorem SimpleGraph.Walk.IsEulerian.card_odd_degree {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] [Fintype V] [DecidableRel G.Adj] {u : V} {v : V} {p : SimpleGraph.Walk G u v} (ht : SimpleGraph.Walk.IsEulerian p) : Fintype.card ↑{v : V | Odd (SimpleGraph.degree G v)} = 0 ∨ Fintype.card ↑{v : V | Odd (SimpleGraph.degree G v)} = 2