sum_incMatrix_apply_of_notMem_edgeSet

English

If e is not an edge of G, then the sum over all vertices a of G.incMatrix R a e is zero.

Русский

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

LaTeX

$$$\forall {R} {\alpha} (G : SimpleGraph \alpha) [Fintype \alpha], e \notin G.edgeSet \Rightarrow Finset.univ.sum (fun a => G.incMatrix R a e) = 0$$$

Lean4

theorem sum_incMatrix_apply_of_notMem_edgeSet [Fintype α] (h : e ∉ G.edgeSet) : ∑ a, G.incMatrix R a e = 0 :=
  sum_eq_zero fun _ _ => G.incMatrix_of_notMem_incidenceSet fun he => h he.1

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