incMatrix_apply — Mathlib

English

The entry (a,e) of the incidence matrix equals the indicator of incidence of e with a.

Русский

Элемент (a,e) матрицы инцидентности равен индикатору принадлежности ребра e вершине a.

LaTeX

$$$G.incMatrix R a e = (G.incidenceSet a).indicator 1 e$$$

Lean4

theorem incMatrix_apply [Zero R] [One R] [DecidableEq α] [DecidableRel G.Adj] {a : α} {e : Sym2 α} :
    G.incMatrix R a e = (G.incidenceSet a).indicator 1 e := by simp [incMatrix, Set.indicator]

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