sum_incMatrix_apply_of_mem_edgeSet

English

If e is an edge of G (i.e., e ∈ edgeSet G), then summing the incidence matrix entries over all vertices a gives 2, corresponding to the two endpoints of e.

Русский

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

LaTeX

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

Lean4

theorem sum_incMatrix_apply_of_mem_edgeSet [Fintype α] : e ∈ G.edgeSet → ∑ a, G.incMatrix R a e = 2 :=
  by
  refine e.ind ?_
  intro a b h
  rw [mem_edgeSet] at h
  rw [← Nat.cast_two, ← card_pair h.ne]
  simp only [incMatrix_apply', sum_boole, mk'_mem_incidenceSet_iff, h]
  congr 2
  ext e
  simp

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