English
If vertices a and b are adjacent, then the (a,b) entry of incMatrix multiplied by its transpose is 1.
Русский
Если вершины a и b смежны, то элемент (a,b) произведения incMatrix на его транспонированную равен 1.
LaTeX
$$$\forall {a,b} \; G.Adj a b \Rightarrow (G.incMatrix R * (G.incMatrix R)^T) a b = 1$$$
Lean4
theorem incMatrix_mul_transpose_apply_of_adj (h : G.Adj a b) : (G.incMatrix R * (G.incMatrix R)ᵀ) a b = (1 : R) :=
by
simp_rw [Matrix.mul_apply, Matrix.transpose_apply, incMatrix_apply_mul_incMatrix_apply, Set.indicator_apply,
Pi.one_apply, sum_boole]
convert @Nat.cast_one R _
convert card_singleton s(a, b)
rw [← coe_eq_singleton, coe_filter_univ]
exact G.incidenceSet_inter_incidenceSet_of_adj h