dart_card_eq_sum_degrees — Mathlib

English

Let G be a finite simple graph. Then the number of all darts equals the sum of the degrees of all vertices, i.e. |G.Dart| = ∑_v deg_G(v).

Русский

Пусть G — конечный простой граф. Тогда число дуг равно сумме степеней вершин: |G.Dart| = ∑_v deg_G(v).

LaTeX

$$$\lvert G.Dart \rvert = \sum_v G.degree(v)$$$

Lean4

theorem dart_card_eq_sum_degrees : Fintype.card G.Dart = ∑ v, G.degree v :=
  by
  haveI := Classical.decEq V
  simp only [← card_univ, ← dart_fst_fiber_card_eq_degree]
  exact card_eq_sum_card_fiberwise (by simp)

Похожие утверждения