incMatrix_apply' — Mathlib

English

Reiterates that the incidence matrix entry equals the indicator of incidence.

Русский

Повторяется, что элемент матрицы инцидентности равен индикатору принадлежности.

LaTeX

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

Lean4

/-- Entries of the incidence matrix can be computed given additional decidable instances. -/
theorem incMatrix_apply' [Zero R] [One R] [DecidableEq α] [DecidableRel G.Adj] {a : α} {e : Sym2 α} :
    G.incMatrix R a e = if e ∈ G.incidenceSet a then 1 else 0 :=
  rfl

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