Documentation

Mathlib.Combinatorics.SimpleGraph.Trails

Trails and Eulerian trails #

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

Main definitions #

TODO #

Tags #

Eulerian trails

@[reducible, inline]
abbrev SimpleGraph.Walk.IsTrail.edgesFinset {V : Type u_1} {G : SimpleGraph V} {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 : SimpleGraph V} [DecidableEq V] {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 : SimpleGraph V} [DecidableEq V] {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 : SimpleGraph V} [DecidableEq V] {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 : SimpleGraph V} [DecidableEq V] {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 : SimpleGraph V} [DecidableEq V] {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 : SimpleGraph V} [DecidableEq V] {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 : SimpleGraph V} [DecidableEq V] {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 : SimpleGraph V} [DecidableEq V] [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 : SimpleGraph V} [DecidableEq V] {x : V} {u : V} {v : V} {p : G.Walk u v} (ht : p.IsEulerian) [Fintype V] [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 : SimpleGraph V} [DecidableEq V] [Fintype V] [DecidableRel G.Adj] {u : V} {v : V} {p : G.Walk u v} (ht : p.IsEulerian) {s : Finset V} (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 : SimpleGraph V} [DecidableEq V] [Fintype V] [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