incMatrix_of_notMem_incidenceSet — Mathlib

English

Let G be a simple graph with vertex set α over a ring-like structure R. For any vertex a ∈ α and any edge e ∈ Sym2 α, if e is not incident to a (i.e., e ∉ incidenceSet a), then the entry of the incidence matrix at position (a, e) is zero.

Русский

Пусть G — простной граф над множеством вершин α. Для любой вершины a ∈ α и любого ребра e ∈ Sym2 α, если e не инцидидент[a] вершине a (то есть e ∉ incidenceSet a), то соответствующая запись incidence matrix равна 0.

LaTeX

$$$\forall R \; \forall \alpha \; (G : SimpleGraph \alpha) \; (a : \alpha) \; (e : Sym2 \alpha),\; e \notin G.incidenceSet(a) \Rightarrow G.incMatrix R a e = 0$$$

Lean4

theorem incMatrix_of_notMem_incidenceSet (h : e ∉ G.incidenceSet a) : G.incMatrix R a e = 0 := by
  rw [incMatrix_apply, Set.indicator_of_notMem h]

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