SimpleGraph.incMatrix_apply'

theorem SimpleGraph.incMatrix_apply' : ∀ {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [inst : Zero R] [inst_1 : One R] [inst_2 : DecidableEq α] [inst_3 : DecidableRel G.Adj] {a : α} {e : Sym2 α}, SimpleGraph.incMatrix R G a e = if e ∈ G.incidenceSet a then 1 else 0

The theorem `SimpleGraph.incMatrix_apply'` asserts that for any given type `R`, type `α`, a simple graph `G` with vertices of type `α`, and instances of zero and one for type `R` and decidable equality for type `α` and a decidable adjacency relation for graph `G`, the entries of the incidence matrix of the graph can be computed for any vertex `a` of type `α` and an unordered pair of vertices `e` of type `Sym2 α`. Specifically, if `e`, the unordered pair of vertices, belongs to the incidence set of the vertex `a` (i.e., `e` is an edge incident to `a`), the corresponding entry in the incidence matrix is `1`. Otherwise, if `e` is not an edge incident to `a`, the entry is `0`.

More concisely: For a simple graph with decidable vertex type and adjacency relation, the incidence matrix entries equal 1 if the unordered pair of vertices represents an edge incident to a given vertex, and 0 otherwise.