Eulerian circuits

TheoremEdges at a vertex of an Eulerian trail#✓fully proved

Let \(G\) be a finite simple graph and let \(p\) be an Eulerian trail in \(G\), that is, a walk between any two vertices that uses every edge of \(G\) exactly once. Then for every vertex \(x\), the number of edges of \(p\) that contain \(x\), counted with multiplicity along \(p\), equals the degree of \(x\) in \(G\).

public theorem Walk.IsEulerian.countP_edges_eq_degree {V : Type*} [Fintype V]
    [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {u v : V}
    {p : G.Walk u v} (hp : p.IsEulerian) (x : V) :
    p.edges.countP (x ∈ ·) = G.degree x

Used by 2

Used byEuler circuits in edge-indexed multigraphs · Euler circuits in edge-indexed multigraphs whose non-isolated vertices are connected

TheoremEuler circuits in connected even graphs#✓fully proved

Every finite connected simple graph in which every vertex has even degree has a closed Eulerian trail, that is, a closed walk that uses every edge of the graph exactly once.

public theorem Connected.exists_isEulerian {V : Type*} [Fintype V] [DecidableEq V]
    {G : SimpleGraph V} [DecidableRel G.Adj] (hG : G.Connected)
    (heven : ∀ v, Even (G.degree v)) :
    ∃ (u : V) (p : G.Walk u u), p.IsEulerian

Used by 2

Used byEuler circuits in edge-indexed multigraphs · Euler circuits in simple graphs whose non-isolated vertices are connected

TheoremReachability among non-isolated vertices#✓fully proved

Let \(G\) be a simple graph and let \(u\) and \(v\) be non-isolated vertices of \(G\), that is, vertices with at least one neighbour. If \(v\) is reachable from \(u\) in \(G\), then \(v\) is reachable from \(u\) in the subgraph of \(G\) induced on the set of non-isolated vertices.

public theorem Reachable.induce_support {V : Type*} {G : SimpleGraph V}
    {u v : V} (h : G.Reachable u v) (hu : u ∈ G.support) (hv : v ∈ G.support) :
    (G.induce G.support).Reachable ⟨u, hu⟩ ⟨v, hv⟩

Used by 1

Used byEuler circuits in edge-indexed multigraphs whose non-isolated vertices are connected

TheoremEuler circuits in simple graphs whose non-isolated vertices are connected#✓fully proved

Let \(G\) be a finite simple graph in which every vertex has even degree, and suppose that the subgraph of \(G\) induced on its non-isolated vertices is connected (in particular nonempty, so \(G\) has at least one edge). Then \(G\) has a closed Eulerian trail, that is, a closed walk that uses every edge of \(G\) exactly once.

Isolated vertices are irrelevant to an Euler tour.

public theorem ConnectedSupport.exists_isEulerian {V : Type*} [Fintype V]
    [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj]
    (hG : (G.induce G.support).Connected)
    (heven : ∀ v, Even (G.degree v)) :
    ∃ (u : V) (p : G.Walk u u), p.IsEulerian

Uses 1 · Used by 1

Proof usesEuler circuits in connected even graphs

Used byEuler circuits in edge-indexed multigraphs whose non-isolated vertices are connected

StructureEdge-indexed multigraph#✓fully proved

An edge-indexed multigraph with vertex type \(V\) and edge type \(E\) assigns to each edge \(e \in E\) an unordered pair of endpoints in \(V\), such that no edge has two equal endpoints. Distinct edges may have the same endpoints, so parallel edges are distinguished by their elements of \(E\).

public structure EdgeIndexedMultigraph (V : Type*) (E : Type*) where
  /-- The unordered endpoints of an edge. -/
  ends : E → Sym2 V
  /-- No edge has two equal endpoints. -/
  loopless : ∀ e v, ends e ≠ s(v, v)

Used by 35

Used byDegree in an edge-indexed multigraph · Degree as the number of incident edges · Degrees are bounded by the maximum degree · Disjoint sum of edge-indexed multigraphs · Adding edges preserves connectedness · Degrees add under disjoint sums · Endpoints of edges from the first summand · Endpoints of edges from the second summand · Edge list of an indexed walk · Edge list of an extended indexed walk · The empty indexed walk has no edges · Edges of the forgetful walk · Handshake lemma for edge-indexed multigraphs · Euler circuits in edge-indexed multigraphs · Euler circuits in edge-indexed multigraphs whose non-isolated vertices are connected · Degree counts incident edges · Incidence · Incidence is membership in the endpoint pair · Indexed walk · Eulerian indexed walk · Characterization of Eulerian indexed walks · Indexed trail · Characterization of indexed trails · Forgetting edge identities preserves length · Line graph of an edge-indexed multigraph · Adjacency in the line graph of a multigraph · Maximum degree of a multigraph · Vertex list of an indexed walk · Support of a walk extended at the front · Support of the empty indexed walk · Forgetting edge identities preserves the vertex sequence · From an indexed walk to a walk in the underlying graph · Underlying simple graph of an edge-indexed multigraph · Adjacency in the underlying graph · Strengthened Fleischner theorem

InductiveIndexed walk#✓fully proved

In an edge-indexed multigraph, an indexed walk is a walk that records which edge it traverses at each step. Indexed walks are defined inductively: for every vertex \(v\) there is the empty indexed walk from \(v\) to \(v\), and if \(e\) is an edge with endpoints \(u\) and \(v\) and \(p\) is an indexed walk from \(v\) to \(w\), then traversing \(e\) from \(u\) to \(v\) and then following \(p\) is an indexed walk from \(u\) to \(w\).

public inductive IndexedWalk : V → V → Type _
  | nil (v : V) : IndexedWalk v v
  | cons {u v w : V} (e : E) (he : M.ends e = s(u, v))
      (p : IndexedWalk v w) : IndexedWalk u w

Uses 1 · Used by 17

Statement usesEdge-indexed multigraph

Used byEdge list of an indexed walk · Edge list of an extended indexed walk · The empty indexed walk has no edges · Edges of the forgetful walk · Euler circuits in edge-indexed multigraphs · Euler circuits in edge-indexed multigraphs whose non-isolated vertices are connected · Eulerian indexed walk · Characterization of Eulerian indexed walks · Indexed trail · Characterization of indexed trails · Forgetting edge identities preserves length · Vertex list of an indexed walk · Support of a walk extended at the front · Support of the empty indexed walk · Forgetting edge identities preserves the vertex sequence · From an indexed walk to a walk in the underlying graph · Strengthened Fleischner theorem

DefinitionVertex list of an indexed walk#✓fully proved

The support of an indexed walk \(p\) from \(u\) to \(v\) in an edge-indexed multigraph is the list of the vertices that \(p\) visits, in order and with repetitions, including both endpoints: the empty walk at \(w\) has support \([w]\), and a walk that starts at \(u\) with an edge and continues with an indexed walk \(q\) has support \(u\) followed by the support of \(q\).

public def support {u v : V} : M.IndexedWalk u v → List V
  | .nil w => [w]
  | .cons _ _ p => u :: p.support

Uses 2 · Used by 3

Statement usesEdge-indexed multigraph · Indexed walk

Used bySupport of a walk extended at the front · Support of the empty indexed walk · Forgetting edge identities preserves the vertex sequence

DefinitionEdge list of an indexed walk#✓fully proved

The edge list of an indexed walk is the list of the edge identities it traverses, in order and with repetitions: the empty walk has the empty edge list, and the walk that traverses an edge \(e\) and then follows an indexed walk \(p\) has edge list \(e\) followed by the edge list of \(p\).

public def edges {u v : V} : M.IndexedWalk u v → List E
  | .nil _ => []
  | .cons e _ p => e :: p.edges

Uses 2 · Used by 11

Statement usesEdge-indexed multigraph · Indexed walk

Used byEdge list of an extended indexed walk · The empty indexed walk has no edges · Edges of the forgetful walk · Euler circuits in edge-indexed multigraphs · Euler circuits in edge-indexed multigraphs whose non-isolated vertices are connected · Eulerian indexed walk · Characterization of Eulerian indexed walks · Indexed trail · Characterization of indexed trails · Forgetting edge identities preserves length · Strengthened Fleischner theorem

DefinitionIndexed trail#✓fully proved

An indexed walk \(p\) in an edge-indexed multigraph is a trail when its edge list has no repeated entries, that is, \(p\) traverses each edge of the multigraph at most once.

public def IsTrail {u v : V} (p : M.IndexedWalk u v) : Prop :=
  p.edges.Nodup

Uses 3 · Used by 6

Statement usesEdge-indexed multigraph · Indexed walk · Edge list of an indexed walk

Used byEuler circuits in edge-indexed multigraphs · Euler circuits in edge-indexed multigraphs whose non-isolated vertices are connected · Eulerian indexed walk · Characterization of Eulerian indexed walks · Characterization of indexed trails · Strengthened Fleischner theorem

TheoremCharacterization of indexed trails#✓fully proved

An indexed walk is a trail exactly when its edge list has no duplicates.

public theorem isTrail_iff {u v : V} (p : M.IndexedWalk u v) :
    p.IsTrail ↔ p.edges.Nodup

Uses 4

Statement usesEdge-indexed multigraph · Indexed walk · Indexed trail · Edge list of an indexed walk

DefinitionEulerian indexed walk#✓fully proved

An indexed walk is Eulerian when it is a trail, that is, it uses no edge identity twice, and every edge identity of the multigraph occurs in its edge list.

public def IsEulerian {u v : V} (p : M.IndexedWalk u v) : Prop :=
  p.IsTrail ∧ ∀ e, e ∈ p.edges

Uses 4 · Used by 4

Statement usesEdge-indexed multigraph · Indexed walk · Indexed trail · Edge list of an indexed walk

Used byEuler circuits in edge-indexed multigraphs · Euler circuits in edge-indexed multigraphs whose non-isolated vertices are connected · Characterization of Eulerian indexed walks · Strengthened Fleischner theorem

TheoremCharacterization of Eulerian indexed walks#✓fully proved

An indexed walk is Eulerian exactly when it is a trail whose edge list contains every edge identity of the multigraph.

public theorem isEulerian_iff {u v : V} (p : M.IndexedWalk u v) :
    p.IsEulerian ↔ p.IsTrail ∧ ∀ e, e ∈ p.edges

Uses 5

Statement usesEdge-indexed multigraph · Indexed walk · Eulerian indexed walk · Indexed trail · Edge list of an indexed walk

TheoremSupport of the empty indexed walk#✓fully proved

The support of the empty indexed walk at a vertex \(v\) is the one-element list \([v]\).

@[simp]
public theorem support_nil (v : V) : (IndexedWalk.nil v : M.IndexedWalk v v).support = [v]

Uses 3

Statement usesEdge-indexed multigraph · Indexed walk · Vertex list of an indexed walk

TheoremSupport of a walk extended at the front#✓fully proved

If \(e\) is an edge with endpoints \(u\) and \(v\) and \(p\) is an indexed walk starting at \(v\), then the support of the walk that traverses \(e\) from \(u\) to \(v\) and then follows \(p\) is \(u\) followed by the support of \(p\).

@[simp]
public theorem support_cons {u v w : V} (e : E) (he : M.ends e = s(u, v))
    (p : M.IndexedWalk v w) : (IndexedWalk.cons e he p).support = u :: p.support

Uses 3

Statement usesEdge-indexed multigraph · Indexed walk · Vertex list of an indexed walk

TheoremThe empty indexed walk has no edges#✓fully proved

For every vertex \(v\) of an edge-indexed multigraph, the edge list of the empty indexed walk at \(v\) is the empty list.

@[simp]
public theorem edges_nil (v : V) : (IndexedWalk.nil v : M.IndexedWalk v v).edges = []

Uses 3

Statement usesEdge-indexed multigraph · Indexed walk · Edge list of an indexed walk

TheoremEdge list of an extended indexed walk#✓fully proved

Let \(p\) be an indexed walk from \(v\) to \(w\) in an edge-indexed multigraph \(M\), and let \(e\) be an edge of \(M\) with endpoints \(u\) and \(v\). The edge list of the walk from \(u\) to \(w\) that traverses \(e\) and then follows \(p\) is \(e\) followed by the edge list of \(p\).

@[simp]
public theorem edges_cons {u v w : V} (e : E) (he : M.ends e = s(u, v))
    (p : M.IndexedWalk v w) : (IndexedWalk.cons e he p).edges = e :: p.edges

Uses 3 · Used by 1

Statement usesEdge-indexed multigraph · Indexed walk · Edge list of an indexed walk

Used byStrengthened Fleischner theorem

DefinitionIncidence#✓fully proved

In an edge-indexed multigraph, a vertex \(v\) is incident with an edge \(e\) when \(v\) belongs to the unordered pair of endpoints of \(e\).

public def Inc (v : V) (e : E) : Prop :=
  v ∈ M.ends e

Uses 1 · Used by 11

Statement usesEdge-indexed multigraph

Used byDegree in an edge-indexed multigraph · Degree as the number of incident edges · Degrees add under disjoint sums · Handshake lemma for edge-indexed multigraphs · Euler circuits in edge-indexed multigraphs · Euler circuits in edge-indexed multigraphs whose non-isolated vertices are connected · Degree counts incident edges · Incidence is membership in the endpoint pair · Line graph of an edge-indexed multigraph · Adjacency in the line graph of a multigraph · Strengthened Fleischner theorem

TheoremIncidence is membership in the endpoint pair#✓fully proved

In an edge-indexed multigraph, a vertex \(v\) is incident with an edge \(e\) if and only if \(v\) belongs to the unordered pair of endpoints of \(e\).

@[simp]
public theorem inc_iff (v : V) (e : E) : M.Inc v e ↔ v ∈ M.ends e

Uses 2 · Used by 4

Statement usesEdge-indexed multigraph · Incidence

Used byHandshake lemma for edge-indexed multigraphs · Euler circuits in edge-indexed multigraphs · Euler circuits in edge-indexed multigraphs whose non-isolated vertices are connected · Strengthened Fleischner theorem

DefinitionUnderlying simple graph of an edge-indexed multigraph#✓fully proved

The underlying simple graph of an edge-indexed multigraph \(M\) with vertex set \(V\) is the simple graph on \(V\) whose edges are the unordered pairs \(\{u, v\}\) that are the endpoint pair of some edge of \(M\); such pairs have \(u \ne v\) because \(M\) is loopless. It forgets edge multiplicities.

public def underlying : SimpleGraph V :=
  fromEdgeSet (Set.range M.ends)

Uses 1 · Used by 9

Statement usesEdge-indexed multigraph

Used byAdding edges preserves connectedness · Edges of the forgetful walk · Euler circuits in edge-indexed multigraphs · Euler circuits in edge-indexed multigraphs whose non-isolated vertices are connected · Forgetting edge identities preserves length · Forgetting edge identities preserves the vertex sequence · From an indexed walk to a walk in the underlying graph · Adjacency in the underlying graph · Strengthened Fleischner theorem

TheoremAdjacency in the underlying graph#✓fully proved

Let \(M\) be an edge-indexed multigraph. Two vertices \(u\) and \(v\) are adjacent in the underlying simple graph of \(M\) if and only if some edge \(e\) of \(M\) has endpoint pair \(\{u, v\}\).

@[simp]
public theorem underlying_adj {u v : V} :
    M.underlying.Adj u v ↔ ∃ e, M.ends e = s(u, v)

Uses 2 · Used by 5

Statement usesEdge-indexed multigraph · Underlying simple graph of an edge-indexed multigraph

Used byAdding edges preserves connectedness · Euler circuits in edge-indexed multigraphs · Euler circuits in edge-indexed multigraphs whose non-isolated vertices are connected · From an indexed walk to a walk in the underlying graph · Strengthened Fleischner theorem

DefinitionFrom an indexed walk to a walk in the underlying graph#✓fully proved

Let \(M\) be an edge-indexed multigraph. An indexed walk \(p\) in \(M\) from \(u\) to \(v\) yields a walk from \(u\) to \(v\) in the underlying simple graph of \(M\) by forgetting edge identities: the empty indexed walk at \(w\) goes to the empty walk at \(w\), and an indexed walk that first traverses an edge \(e\) with endpoints \(\{u, x\}\) and then continues with an indexed walk \(q\) goes to the walk that first steps from \(u\) to \(x\), an edge of the underlying graph because \(e\) has these endpoints, and then follows the image of \(q\).

public def toWalk {u v : V} : M.IndexedWalk u v → M.underlying.Walk u v
  | .nil w => .nil
  | .cons e he p => .cons (M.underlying_adj.mpr ⟨e, he⟩) p.toWalk

Uses 4 · Used by 4

Statement usesEdge-indexed multigraph · Indexed walk · Underlying simple graph of an edge-indexed multigraph · Adjacency in the underlying graph

Used byEdges of the forgetful walk · Forgetting edge identities preserves length · Forgetting edge identities preserves the vertex sequence · Strengthened Fleischner theorem

TheoremForgetting edge identities preserves the vertex sequence#✓fully proved

Let \(M\) be an edge-indexed multigraph and \(p\) an indexed walk in \(M\) from \(u\) to \(v\). The walk from \(u\) to \(v\) in the underlying simple graph of \(M\) obtained from \(p\) by forgetting edge identities visits the same vertices as \(p\), in the same order: the two supports are equal as lists.

@[simp]
public theorem support_toWalk {u v : V} (p : M.IndexedWalk u v) :
    p.toWalk.support = p.support

Uses 5

Statement usesEdge-indexed multigraph · Indexed walk · Vertex list of an indexed walk · From an indexed walk to a walk in the underlying graph · Underlying simple graph of an edge-indexed multigraph

TheoremEdges of the forgetful walk#✓fully proved

For every indexed walk \(p\) from \(u\) to \(v\) in an edge-indexed multigraph, the edge list of the walk in the underlying simple graph obtained from \(p\) by forgetting edge identities is the list of the endpoint pairs of the edges of \(p\), taken in the same order.

@[simp]
public theorem edges_toWalk {u v : V} (p : M.IndexedWalk u v) :
    p.toWalk.edges = p.edges.map M.ends

Uses 5 · Used by 2

Statement usesEdge-indexed multigraph · Indexed walk · Edge list of an indexed walk · From an indexed walk to a walk in the underlying graph · Underlying simple graph of an edge-indexed multigraph

Used byForgetting edge identities preserves length · Strengthened Fleischner theorem

TheoremForgetting edge identities preserves length#✓fully proved

For an indexed walk \(p\), the walk in the underlying simple graph obtained by forgetting edge identities has the same length as \(p\), namely the number of entries in the edge list of \(p\).

@[simp]
public theorem length_toWalk {u v : V} (p : M.IndexedWalk u v) :
    p.toWalk.length = p.edges.length

Uses 6 · Used by 1

Statement usesEdge-indexed multigraph · Indexed walk · Edge list of an indexed walk · From an indexed walk to a walk in the underlying graph · Underlying simple graph of an edge-indexed multigraph

Proof usesEdges of the forgetful walk

Used byStrengthened Fleischner theorem

DefinitionDegree in an edge-indexed multigraph#✓fully proved

The degree of a vertex \(v\) in an edge-indexed multigraph \(M\) is the number of edges of \(M\) incident with \(v\), that is, the cardinality of the set of edges whose endpoint pair contains \(v\); it is defined to be \(0\) when this set is infinite.

public noncomputable def degree (v : V) : ℕ :=
  {e | M.Inc v e}.ncard

Uses 2 · Used by 9

Statement usesEdge-indexed multigraph · Incidence

Used byDegree as the number of incident edges · Degrees are bounded by the maximum degree · Degrees add under disjoint sums · Handshake lemma for edge-indexed multigraphs · Euler circuits in edge-indexed multigraphs · Euler circuits in edge-indexed multigraphs whose non-isolated vertices are connected · Degree counts incident edges · Maximum degree of a multigraph · Strengthened Fleischner theorem

TheoremDegree as the number of incident edges#✓fully proved

For every vertex \(v\) of an edge-indexed multigraph \(M\), the degree of \(v\) equals the cardinality of the set of edges of \(M\) whose endpoint pair contains \(v\), where this cardinality is taken to be \(0\) when the set is infinite.

public theorem degree_eq_ncard_inc (v : V) :
    M.degree v = {e | M.Inc v e}.ncard

Uses 3

Statement usesEdge-indexed multigraph · Incidence · Degree in an edge-indexed multigraph

DefinitionDisjoint sum of edge-indexed multigraphs#✓fully proved

Given edge-indexed multigraphs \(M\) and \(N\) on the same vertex type \(V\), with edge types \(E\) and \(F\), their disjoint sum is the edge-indexed multigraph on \(V\) whose edge type is the disjoint union \(E \sqcup F\), where an edge coming from \(E\) has its endpoints in \(M\) and an edge coming from \(F\) has its endpoints in \(N\).

public def disjointSum {F : Type*} (N : EdgeIndexedMultigraph V F) :
    EdgeIndexedMultigraph V (E ⊕ F) where
  ends
    | Sum.inl e => M.ends e
    | Sum.inr f => N.ends f
  loopless := by
    intro e v
    cases e with
    | inl e => exact M.loopless e v
    | inr f => exact N.loopless f v

Uses 1 · Used by 5

Statement usesEdge-indexed multigraph

Used byAdding edges preserves connectedness · Degrees add under disjoint sums · Endpoints of edges from the first summand · Endpoints of edges from the second summand · Strengthened Fleischner theorem

TheoremEndpoints of edges from the first summand#✓fully proved

Let \(M\) and \(N\) be edge-indexed multigraphs on the same vertex type. Every edge \(e\) of \(M\), viewed as an edge of the disjoint sum of \(M\) and \(N\), has the same endpoints as in \(M\).

@[simp]
public theorem disjointSum_ends_inl {F : Type*} (N : EdgeIndexedMultigraph V F) (e : E) :
    (M.disjointSum N).ends (Sum.inl e) = M.ends e

Uses 2

Statement usesEdge-indexed multigraph · Disjoint sum of edge-indexed multigraphs

TheoremEndpoints of edges from the second summand#✓fully proved

Let \(M\) and \(N\) be edge-indexed multigraphs on the same vertex type. Every edge \(f\) of \(N\), viewed as an edge of the disjoint sum of \(M\) and \(N\), has the same endpoints as in \(N\).

@[simp]
public theorem disjointSum_ends_inr {F : Type*} (N : EdgeIndexedMultigraph V F) (f : F) :
    (M.disjointSum N).ends (Sum.inr f) = N.ends f

Uses 2

Statement usesEdge-indexed multigraph · Disjoint sum of edge-indexed multigraphs

TheoremDegrees add under disjoint sums#✓fully proved

Let \(M\) and \(N\) be edge-indexed multigraphs on the same vertex type, each with finitely many edges. Then for every vertex \(v\), the degree of \(v\) in the disjoint sum of \(M\) and \(N\) equals the degree of \(v\) in \(M\) plus the degree of \(v\) in \(N\).

public theorem disjointSum_degree {F : Type*} [Finite E] [Finite F]
    (N : EdgeIndexedMultigraph V F) (v : V) :
    (M.disjointSum N).degree v = M.degree v + N.degree v

Uses 4 · Used by 1

Statement usesEdge-indexed multigraph · Degree in an edge-indexed multigraph · Disjoint sum of edge-indexed multigraphs

Proof usesIncidence

Used byStrengthened Fleischner theorem

TheoremAdding edges preserves connectedness#✓fully proved

Let \(M\) and \(N\) be edge-indexed multigraphs on the same vertex type. If the underlying simple graph of \(M\) is connected, then the underlying simple graph of the disjoint sum of \(M\) and \(N\) is connected.

public theorem disjointSum_connected_left {F : Type*}
    (N : EdgeIndexedMultigraph V F) (hM : M.underlying.Connected) :
    (M.disjointSum N).underlying.Connected

Uses 4

Statement usesEdge-indexed multigraph · Disjoint sum of edge-indexed multigraphs · Underlying simple graph of an edge-indexed multigraph

Proof usesAdjacency in the underlying graph

TheoremHandshake lemma for edge-indexed multigraphs#✓fully proved

In an edge-indexed multigraph with finitely many vertices and finitely many edges, the sum of the degrees of all vertices is even.

public theorem even_sum_degree [Fintype V] [Finite E] :
    Even (∑ v, M.degree v)

Uses 4 · Used by 1

Statement usesEdge-indexed multigraph · Degree in an edge-indexed multigraph

Proof usesIncidence · Incidence is membership in the endpoint pair

Used byStrengthened Fleischner theorem

TheoremEuler circuits in edge-indexed multigraphs#✓fully proved

Let \(M\) be an edge-indexed multigraph with finitely many vertices and finitely many edges. If the underlying simple graph of \(M\) is connected and every vertex of \(M\) has even degree, then there are a vertex \(u\) and a closed indexed walk from \(u\) to \(u\) that is Eulerian, that is, it traverses every edge of \(M\) exactly once.

public theorem exists_indexedEulerian [Finite V] [Finite E]
    (hconn : M.underlying.Connected) (heven : ∀ v, Even (M.degree v)) :
    ∃ (u : V) (p : M.IndexedWalk u u), p.IsEulerian

Uses 12 · Used by 1

Statement usesEdge-indexed multigraph · Indexed walk · Eulerian indexed walk · Degree in an edge-indexed multigraph · Underlying simple graph of an edge-indexed multigraph

Proof usesEuler circuits in connected even graphs · Incidence · Indexed trail · Edge list of an indexed walk · Incidence is membership in the endpoint pair · Adjacency in the underlying graph · Edges at a vertex of an Eulerian trail

Used byStrengthened Fleischner theorem

TheoremEuler circuits in edge-indexed multigraphs whose non-isolated vertices are connected#✓fully proved

Let \(M\) be an edge-indexed multigraph with finitely many vertices and finitely many edges. Suppose that the subgraph of the underlying simple graph of \(M\) induced on its non-isolated vertices is connected, and that every vertex of \(M\) has even degree. Then there are a vertex \(u\) and a closed indexed walk from \(u\) to \(u\) that is Eulerian, that is, it traverses every edge of \(M\) exactly once.

A connected graph has at least one vertex, so the hypothesis requires \(M\) to have an edge.

public theorem exists_indexedEulerian_connectedSupport [Finite V] [Finite E]
    (hconn : (M.underlying.induce M.underlying.support).Connected)
    (heven : ∀ v, Even (M.degree v)) :
    ∃ (u : V) (p : M.IndexedWalk u u), p.IsEulerian

Uses 13

Statement usesEdge-indexed multigraph · Indexed walk · Eulerian indexed walk · Degree in an edge-indexed multigraph · Underlying simple graph of an edge-indexed multigraph

Proof usesEuler circuits in simple graphs whose non-isolated vertices are connected · Incidence · Indexed trail · Edge list of an indexed walk · Incidence is membership in the endpoint pair · Adjacency in the underlying graph · Reachability among non-isolated vertices · Edges at a vertex of an Eulerian trail

DefinitionLine graph of an edge-indexed multigraph#✓fully proved

The line graph of an edge-indexed multigraph is the simple graph whose vertices are the edge identities, two of them being adjacent when they are distinct and share an endpoint. In particular, parallel edges are adjacent.

public def lineGraph : SimpleGraph E where
  Adj e₁ e₂ := e₁ ≠ e₂ ∧ ∃ v, M.Inc v e₁ ∧ M.Inc v e₂
  symm := ⟨by
    intro e₁ e₂ h
    obtain ⟨hne, v, hv₁, hv₂⟩ := h
    exact ⟨Ne.symm hne, v, hv₂, hv₁⟩⟩
  loopless := ⟨by
    intro e h
    exact h.1 rfl⟩

Uses 2 · Used by 1

Statement usesEdge-indexed multigraph · Incidence

Used byAdjacency in the line graph of a multigraph

TheoremAdjacency in the line graph of a multigraph#✓fully proved

Two edge identities \(e_1\) and \(e_2\) are adjacent in the line graph of an edge-indexed multigraph exactly when \(e_1 \ne e_2\) and some vertex is incident with both of them.

@[simp]
public theorem lineGraph_adj {e₁ e₂ : E} :
    M.lineGraph.Adj e₁ e₂ ↔ e₁ ≠ e₂ ∧ ∃ v, M.Inc v e₁ ∧ M.Inc v e₂

Uses 3

Statement usesEdge-indexed multigraph · Incidence · Line graph of an edge-indexed multigraph

DefinitionMaximum degree of a multigraph#✓fully proved

For an edge-indexed multigraph with finitely many vertices and finitely many edge identities, the maximum degree is the largest degree of a vertex, and \(0\) when there are no vertices.

Finiteness of the edge identities matters: the degree of a vertex is the cardinality of its set of incident edges, which is taken to be \(0\) for an infinite set, so without it a vertex of infinite degree could be reported as having degree \(0\).

public noncomputable def maxDegree [Fintype V] [Finite E] : ℕ :=
  Finset.univ.sup M.degree

Uses 2 · Used by 1

Statement usesEdge-indexed multigraph · Degree in an edge-indexed multigraph

Used byDegrees are bounded by the maximum degree

TheoremDegrees are bounded by the maximum degree#✓fully proved

Let \(M\) be an edge-indexed multigraph with finitely many vertices and finitely many edges. Then every vertex of \(M\) has degree at most the maximum degree of \(M\).

public theorem degree_le_maxDegree [Fintype V] [Finite E] (v : V) :
    M.degree v ≤ M.maxDegree

Uses 3

Statement usesEdge-indexed multigraph · Degree in an edge-indexed multigraph · Maximum degree of a multigraph

TheoremDegree counts incident edges#✓fully proved

In an edge-indexed multigraph with finitely many edges, the degree of every vertex \(v\) equals the number of edges incident with \(v\).

public theorem filter_inc_card [Fintype E] (v : V)
    [DecidablePred fun e => M.Inc v e] :
    (Finset.univ.filter (fun e => M.Inc v e)).card = M.degree v

Uses 3

Statement usesEdge-indexed multigraph · Incidence · Degree in an edge-indexed multigraph

39 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.