sum_incMatrix_apply — Mathlib

English

For a fixed vertex a, the sum over all edges e of the incidence matrix entries G.incMatrix R a e equals the degree of a.

Русский

Для фиксированной вершины a сумма по всем ребрам e записей инцидентной матрицы равна степени вершины a.

LaTeX

$$$\forall {R} {\alpha} (G : SimpleGraph \alpha) [Fintype (Sym2 \alpha)] {a : \alpha},\; Finset.univ.sum (fun e => G.incMatrix R a e) = G.degree a$$$

Lean4

theorem sum_incMatrix_apply [Fintype (Sym2 α)] [Fintype (neighborSet G a)] : ∑ e, G.incMatrix R a e = G.degree a := by
  simp [incMatrix_apply', sum_boole, Set.filter_mem_univ_eq_toFinset]

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