incMatrix_apply_mul_incMatrix_apply_of_not_adj

English

If a ≠ b and a is not adjacent to b, the product of their incidence entries is zero for any edge e.

Русский

Если a ≠ b и вершины не смежны, произведение инцидентности по любому ребру равно нулю.

LaTeX

$$$(hab : a \neq b) (h : ¬G.Adj a b) : G.incMatrix R a e * G.incMatrix R b e = 0$$$

Lean4

theorem incMatrix_apply_mul_incMatrix_apply_of_not_adj (hab : a ≠ b) (h : ¬G.Adj a b) :
    G.incMatrix R a e * G.incMatrix R b e = 0 :=
  by
  rw [incMatrix_apply_mul_incMatrix_apply, Set.indicator_of_notMem]
  rw [G.incidenceSet_inter_incidenceSet_of_not_adj h hab]
  exact Set.notMem_empty e

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