Degree and the handshake lemma

Degree counting on Mathlib's multigraph Graph α β, for graphs with finitely many vertices and finitely many edges.

Carrying finiteness

V(G) and E(G) are Set α and Set β, not types, so finiteness has to be carried somehow. The choice made here — and inherited by every later graph module — is a Prop-valued class

class Graph.Finite (G : Graph α β) : Prop

bundling V(G).Finite and E(G).Finite, with G.vertexFinset and G.edgeFinset derived from it. The reasons:

• It is a Prop, so it is proof irrelevant. G.vertexFinset and G.degree therefore do not depend on which finiteness proof is in scope, and two lemmas proved with different instances still compose. A bundled Finset-valued structure would not have that property: it duplicates the vertexSet data and forces a ↑G.vertexFinset = V(G) side condition at every call site.
• It is a class, so it is silent at the call site — the statements below read like ordinary graph theory instead of dragging two Set.Finite hypotheses through every signature. The price is that a subgraph does not get an instance for free; Graph.Finite.of_le produces one, and haveI installs it locally. That is the right trade: in this development finiteness is a standing assumption on the ambient graph and subgraphs are formed constantly.
• Finite ↥V(G) and Finite ↥E(G) instances are provided too, so Mathlib's own machinery (Set.Finite.subset, Set.toFinite, ...) fires without help.

Counts are Set.ncard. Set.ncard is total — it is 0 on an infinite set — so G.degree is defined for every graph and needs no instance argument; finiteness enters only where a theorem actually needs it.

Degree

G.degree x is the number of edge ends at x:

G.degree x = (G.incidenceSet x).ncard + (G.loopSet x).ncard

A non-loop edge at x is counted once, by the first summand. A loop at x is counted twice, once by each summand. This is the definition the handshake lemma needs, and it agrees with SimpleGraph.degree on loopless graphs.

Blueprint

• Graph.sum_degree_eq_two_mul_ncard_edgeSet — "the degree sum is twice the number of edges", the counting step in the proof of Lemma lem:three-leaf-tree (Trees with three leaves). The whole content is Graph.ncard_inc_add_ncard_isLoopAt: an edge has exactly two ends.
• Graph.IsLeaf — "the vertices of degree one are the leaves", same lemma.

Namespace

Everything lives in the root Graph namespace rather than in Schoenflies, so that dot notation G.degree, G.IsLeaf, G.vertexFinset works on a G : Graph α β. Later graph modules should do the same.

Finiteness

class Graph.Finite {α : Type u_1} {β : Type u_2} (G : Graph α β) : Prop

G.Finite says that the multigraph G has finitely many vertices and finitely many edges. Both halves are needed: the vertex set does not bound the edge set (parallel edges) and the edge set does not bound the vertex set (isolated vertices).

• finite_vertexSet : G.vertexSet.Finite

  A finite graph has finitely many vertices.

• finite_edgeSet : G.edgeSet.Finite

  A finite graph has finitely many edges.

theorem Graph.finite_vertexSet {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Finite] : G.vertexSet.Finite

theorem Graph.finite_edgeSet {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Finite] : G.edgeSet.Finite

instance Graph.instFiniteElemVertexSetOfFinite {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] : _root_.Finite ↑G.vertexSet

instance Graph.instFiniteElemEdgeSetOfFinite {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] : _root_.Finite ↑G.edgeSet

theorem Graph.Finite.of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H ≤ G) [G.Finite] : H.Finite

A subgraph of a finite graph is finite. This is not an instance — H cannot be recovered from the goal — so install it with let _ := Graph.Finite.of_le h.

noncomputable def Graph.vertexFinset {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Finite] : Finset α

The vertex set of a finite graph, as a Finset.

Equations

• G.vertexFinset = ⋯.toFinset

noncomputable def Graph.edgeFinset {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Finite] : Finset β

The edge set of a finite graph, as a Finset.

Equations

• G.edgeFinset = ⋯.toFinset

@[simp]

theorem Graph.mem_vertexFinset {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} [G.Finite] : x ∈ G.vertexFinset ↔ x ∈ G.vertexSet

@[simp]

theorem Graph.mem_edgeFinset {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} [G.Finite] : e ∈ G.edgeFinset ↔ e ∈ G.edgeSet

@[simp]

theorem Graph.coe_vertexFinset {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] : ↑G.vertexFinset = G.vertexSet

@[simp]

theorem Graph.coe_edgeFinset {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] : ↑G.edgeFinset = G.edgeSet

@[simp]

theorem Graph.card_vertexFinset {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] : G.vertexFinset.card = G.vertexSet.ncard

@[simp]

theorem Graph.card_edgeFinset {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] : G.edgeFinset.card = G.edgeSet.ncard

Incidence sets, unfolded

theorem Graph.incidenceSet_eq_setOf {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) : incidenceSet x = {e : β | G.Inc e x}

theorem Graph.loopSet_eq_setOf {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) : loopSet x = {e : β | G.IsLoopAt e x}

theorem Graph.finite_incidenceSet {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] (x : α) : (incidenceSet x).Finite

theorem Graph.finite_loopSet {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] (x : α) : (loopSet x).Finite

Degree

noncomputable def Graph.degree {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) : ℕ

G.degree x is the number of edge ends of G at the vertex x: a non-loop edge incident with x contributes one, a loop at x contributes two.

Equations

• G.degree x = (Graph.incidenceSet x).ncard + (Graph.loopSet x).ncard

theorem Graph.degree_def {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) : G.degree x = (incidenceSet x).ncard + (loopSet x).ncard

@[simp]

theorem Graph.degree_eq_zero_of_notMem {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (h : x ∉ G.vertexSet) : G.degree x = 0

A vertex outside the graph has no edge ends.

theorem Graph.ncard_loopSet_le_ncard_incidenceSet {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] (x : α) : (loopSet x).ncard ≤ (incidenceSet x).ncard

Loops are counted among the incident edges as well, so they never make the loop term the larger of the two.

theorem Graph.ncard_incidenceSet_le_degree {α : Type u_1} {β : Type u_2} {G : Graph α β} (x : α) : (incidenceSet x).ncard ≤ G.degree x

theorem Graph.degree_eq_ncard_incidenceSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (h : ∀ (e : β), ¬G.IsLoopAt e x) : G.degree x = (incidenceSet x).ncard

On a loopless vertex the degree is just the number of incident edges.

theorem Graph.IsLoopAt.two_le_degree {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} {x : α} [G.Finite] (h : G.IsLoopAt e x) : 2 ≤ G.degree x

A loop at x contributes two to the degree of x.

theorem Graph.degree_pos_of_inc {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} {x : α} [G.Finite] (h : G.Inc e x) : 0 < G.degree x

theorem Graph.degree_eq_zero_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} [G.Finite] : G.degree x = 0 ↔ ∀ (e : β), ¬G.Inc e x

An edge has exactly two ends

This is the entire content of the handshake lemma: summed over the vertices, the number of ends an edge has there is two, whether the edge is a loop (two ends at one vertex) or not (one end at each of two vertices).

theorem Graph.ncard_inc_add_ncard_isLoopAt {α : Type u_1} {β : Type u_2} {e : β} (G : Graph α β) (he : e ∈ G.edgeSet) : {x : α | G.Inc e x}.ncard + {x : α | G.IsLoopAt e x}.ncard = 2

An edge of G has exactly two ends: the vertices it is incident with, counted again at the vertex it is a loop at, total two.

The handshake lemma

theorem Graph.sum_degree_eq_two_mul_ncard_edgeSet {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Finite] : ∑ x ∈ G.vertexFinset, G.degree x = 2 * G.edgeSet.ncard

The handshake lemma. The degrees of the vertices of a finite multigraph add up to twice the number of edges.

The proof is the double count: G.degree x is a sum over the edges of the number of ends that edge has at x, the two sums commute, and each edge contributes exactly two (Graph.ncard_inc_add_ncard_isLoopAt). Loops are allowed — that is exactly what the loop term in Graph.degree buys.

theorem Graph.sum_degree_eq_two_mul_card_edgeFinset {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Finite] : ∑ x ∈ G.vertexFinset, G.degree x = 2 * G.edgeFinset.card

The handshake lemma, with the edge count as a Finset cardinality.

theorem Graph.even_sum_degree {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Finite] : Even (∑ x ∈ G.vertexFinset, G.degree x)

The degree sum of a finite multigraph is even.

Leaves

def Graph.IsLeaf {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) : Prop

G.IsLeaf x says that x is a vertex of G with exactly one edge end at it.

Equations

• G.IsLeaf x = (x ∈ G.vertexSet ∧ G.degree x = 1)

theorem Graph.IsLeaf.mem_vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (h : G.IsLeaf x) : x ∈ G.vertexSet

theorem Graph.IsLeaf.degree_eq_one {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (h : G.IsLeaf x) : G.degree x = 1

theorem Graph.isLeaf_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} : G.IsLeaf x ↔ x ∈ G.vertexSet ∧ G.degree x = 1

theorem Graph.IsLeaf.not_isLoopAt {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} [G.Finite] (h : G.IsLeaf x) (e : β) : ¬G.IsLoopAt e x

A leaf carries no loop: a loop would contribute two to the degree.

theorem Graph.IsLeaf.ncard_incidenceSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} [G.Finite] (h : G.IsLeaf x) : (incidenceSet x).ncard = 1

The one edge end at a leaf comes from one incident edge.

theorem Graph.IsLeaf.loopSet_eq_empty {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} [G.Finite] (h : G.IsLeaf x) : loopSet x = ∅

theorem Graph.IsLeaf.existsUnique_inc {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} [G.Finite] (h : G.IsLeaf x) : ∃! e : β, G.Inc e x

A leaf is incident with exactly one edge.

theorem Graph.IsLeaf.exists_isLink {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} [G.Finite] (h : G.IsLeaf x) : ∃ (e : β) (y : α), y ≠ x ∧ G.IsLink e x y

The unique edge at a leaf is not a loop, so it has a second, different end.

theorem Graph.IsLeaf.isNonloopAt {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} {x : α} [G.Finite] (h : G.IsLeaf x) (he : G.Inc e x) : G.IsNonloopAt e x

Every edge at a leaf is a non-loop edge there.

theorem Graph.isLeaf_of_isNonloopAt {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} {x : α} (hx : x ∈ G.vertexSet) (h : ∀ (f : β), G.Inc f x ↔ f = e) (hne : G.IsNonloopAt e x) : G.IsLeaf x

The converse of the two lemmas above: a vertex of G whose only incident edge is e, and for which e is not a loop, is a leaf.