mathlib documentation

combinatorics.simple_graph.degree_sum

Degree-sum formula and handshaking lemma #

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 #

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

theorem simple_graph.dart.ext_iff {V : Type u} {G : simple_graph V} (x y : G.dart) :
x = y x.fst = y.fst x.snd = y.snd
theorem simple_graph.dart.ext {V : Type u} {G : simple_graph V} (x y : G.dart) (h : x.fst = y.fst) (h_1 : x.snd = y.snd) :
x = y
@[ext]
structure simple_graph.dart {V : Type u} (G : simple_graph V) :
Type u

A dart is a directed edge, consisting of an ordered pair of adjacent vertices.

@[instance]
@[instance]
Equations
def simple_graph.dart.edge {V : Type u} {G : simple_graph V} (d : G.dart) :

The edge associated to the dart.

Equations
@[simp]
theorem simple_graph.dart.edge_mem {V : Type u} {G : simple_graph V} (d : G.dart) :
def simple_graph.dart.rev {V : Type u} {G : simple_graph V} (d : G.dart) :

The dart with reversed orientation from a given dart.

Equations
@[simp]
theorem simple_graph.dart.rev_edge {V : Type u} {G : simple_graph V} (d : G.dart) :
@[simp]
theorem simple_graph.dart.rev_rev {V : Type u} {G : simple_graph V} (d : G.dart) :
d.rev.rev = d
theorem simple_graph.dart.rev_ne {V : Type u} {G : simple_graph V} (d : G.dart) :
d.rev d
theorem simple_graph.dart_edge_eq_iff {V : Type u} {G : simple_graph V} (d₁ d₂ : G.dart) :
d₁.edge = d₂.edge d₁ = d₂ d₁ = d₂.rev
def simple_graph.dart_of_neighbor_set {V : Type u} (G : simple_graph V) (v : V) (w : (G.neighbor_set v)) :

For a given vertex v, this is the bijective map from the neighbor set at v to the darts d with d.fst = v. -

Equations
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.fst = v) finset.univ).card = G.degree v
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 = ∑ (v : V), G.degree v
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.rev}
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 G.edge_set) :
(finset.filter (λ (d : G.dart), d.edge = e) finset.univ).card = 2
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] :
∑ (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.

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
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)