SimpleGraph.sum_degrees_eq_twice_card_edges
theorem SimpleGraph.sum_degrees_eq_twice_card_edges :
∀ {V : Type u} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [inst_2 : Fintype (Sym2 V)],
(Finset.univ.sum fun v => G.degree v) = 2 * G.edgeFinset.card
This theorem is known as the degree-sum formula, or handshaking lemma. It states that for any SimpleGraph `G` over a finite set of vertices `V`, if `Adj` is a decidable relation and the symmetric square of `V` is finite, then the sum of the degrees of all vertices in the graph (computed as the sum of the degrees of each vertex over the entire set of vertices) is equal to twice the number of edges in the graph. In other words, the total number of "connections" in the graph (counted by summing the degrees of vertices) is just twice the total number of edges, since each edge connects two vertices.
More concisely: For any simple graph with finite, decidable adjacency relation, the sum of vertex degrees equals twice the number of edges.
|
SimpleGraph.even_card_odd_degree_vertices
theorem SimpleGraph.even_card_odd_degree_vertices :
∀ {V : Type u} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj],
Even (Finset.filter (fun v => Odd (G.degree v)) Finset.univ).card
The theorem `SimpleGraph.even_card_odd_degree_vertices` states that for any simple graph `G` with a finite set of vertices `V`, where the adjacency relationship `G.Adj` is a decidable relation, the number of vertices with odd degree is even. This is also known as the handshaking lemma, which stipulates that in any graph, the sum of the degrees of all vertices is twice the number of edges, implying that the number of vertices with odd degree must be even. In more formal terms, `Even (Finset.filter (fun v => Odd (G.degree v)) Finset.univ).card` means that the cardinality of the set of vertices `v` such that the degree of `v` is odd (represented as `Odd (G.degree v)`) is an even number. The set of all vertices is represented as `Finset.univ`.
More concisely: The number of vertices in a finite, simple graph with a decidable adjacency relation having odd degree is even.
|