incMatrix_mul_transpose_apply_of_adj

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

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