Degree-sum formula and handshaking lemma #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The degree-sum formula is that the sum of the degrees of the vertices in a finite graph is equal to twice the number of edges. The handshaking lemma, a corollary, is that the number of odd-degree vertices is even.

Main definitions #

simple_graph.sum_degrees_eq_twice_card_edges is the degree-sum formula.
simple_graph.even_card_odd_degree_vertices is the handshaking lemma.
simple_graph.odd_card_odd_degree_vertices_ne is that the number of odd-degree vertices different from a given odd-degree vertex is odd.
simple_graph.exists_ne_odd_degree_of_exists_odd_degree is that the existence of an odd-degree vertex implies the existence of another one.

Implementation notes #

We give a combinatorial proof by using the facts that (1) the map from darts to vertices is such that each fiber has cardinality the degree of the corresponding vertex and that (2) the map from darts to edges is 2-to-1.

Tags #

simple graphs, sums, degree-sum formula, handshaking lemma

source

theorem simple_graph.dart_fst_fiber {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] [decidable_eq V] (v : V) :

finset.filter (λ (d : G.dart), d.to_prod.fst = v) finset.univ = finset.image (G.dart_of_neighbor_set v) finset.univ

source

theorem simple_graph.dart_fst_fiber_card_eq_degree {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] [decidable_eq V] (v : V) :

(finset.filter (λ (d : G.dart), d.to_prod.fst = v) finset.univ).card = G.degree v

source

theorem simple_graph.dart_card_eq_sum_degrees {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] :

fintype.card G.dart = finset.univ.sum (λ (v : V), G.degree v)

source

theorem simple_graph.dart.edge_fiber {V : Type u} {G : simple_graph V} [fintype V] [decidable_rel G.adj] [decidable_eq V] (d : G.dart) :

finset.filter (λ (d' : G.dart), d'.edge = d.edge) finset.univ = {d, d.symm}

source

theorem simple_graph.dart_edge_fiber_card {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] [decidable_eq V] (e : sym2 V) (h : e ∈ ⇑simple_graph.edge_set G) :

(finset.filter (λ (d : G.dart), d.edge = e) finset.univ).card = 2

source

theorem simple_graph.dart_card_eq_twice_card_edges {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] [decidable_eq V] :

fintype.card G.dart = 2 * G.edge_finset.card

source

theorem simple_graph.sum_degrees_eq_twice_card_edges {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] [decidable_eq V] :

finset.univ.sum (λ (v : V), G.degree v) = 2 * G.edge_finset.card

The degree-sum formula. This is also known as the handshaking lemma, which might more specifically refer to simple_graph.even_card_odd_degree_vertices.

source

theorem simple_graph.even_card_odd_degree_vertices {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] :

even (finset.filter (λ (v : V), odd (G.degree v)) finset.univ).card

The handshaking lemma. See also simple_graph.sum_degrees_eq_twice_card_edges.

source

theorem simple_graph.odd_card_odd_degree_vertices_ne {V : Type u} (G : simple_graph V) [fintype V] [decidable_eq V] [decidable_rel G.adj] (v : V) (h : odd (G.degree v)) :

odd (finset.filter (λ (w : V), w ≠ v ∧ odd (G.degree w)) finset.univ).card

source

theorem simple_graph.exists_ne_odd_degree_of_exists_odd_degree {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] (v : V) (h : odd (G.degree v)) :

∃ (w : V), w ≠ v ∧ odd (G.degree w)