incMatrix — Mathlib

English

The incidence matrix G.incMatrix R records which edges are incident to which vertices.

Русский

Матрица инцидентности G.incMatrix R фиксирует, какие ребра инцидентны вершинам.

LaTeX

$$$G.incMatrix R : Matrix α (Sym2 α) R$ определена как $a,e \mapsto 1$ если $e \in G.incidenceSet a$, иначе $0$.$$

Lean4

/-- `G.incMatrix R` is the `α × Sym2 α` matrix whose `(a, e)`-entry is `1` if `e` is incident to
`a` and `0` otherwise. -/
def incMatrix [Zero R] [One R] [DecidableEq α] [DecidableRel G.Adj] : Matrix α (Sym2 α) R :=
  .of fun a e => if e ∈ G.incidenceSet a then 1 else 0

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