incMatrix_of_mem_incidenceSet — Mathlib

English

Let G be a simple graph with incidence structure. If an edge e is incident to a vertex a (i.e., e ∈ incidenceSet a), then the entry of the incidence matrix at (a, e) is one.

Русский

Пусть G — простой граф с инцидентной структурой. Ребро e инцидирует вершину a тогда и только тогда, когда e ∈ incidenceSet a; тогда запись incMatrix R a e равна 1.

LaTeX

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

Lean4

theorem incMatrix_of_mem_incidenceSet (h : e ∈ G.incidenceSet a) : G.incMatrix R a e = 1 := by
  rw [incMatrix_apply, Set.indicator_of_mem h, Pi.one_apply]

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