incMatrix_apply_eq_zero_iff — Mathlib

English

Assume R is a nontrivial ring-like structure. Then the incidence-matrix entry G.incMatrix R a e is zero exactly when e is not in incidenceSet a.

Русский

Пусть R не тривиальная кольцевая структура. Тогда элемент матрицы инцидентности G.incMatrix R a e равен нулю тогда и только тогда, когда e не принадлежит incindenceSet a.

LaTeX

$$$\forall {R} {\alpha} (G : SimpleGraph \alpha) [__Nontrivial R] \; {a : \alpha} {e : Sym2 \alpha},\; G.incMatrix R a e = 0 \iff e \notin G.incidenceSet(a)$$$

Lean4

theorem incMatrix_apply_eq_zero_iff : G.incMatrix R a e = 0 ↔ e ∉ G.incidenceSet a := by
  simp only [incMatrix_apply, Set.indicator_apply_eq_zero, Pi.one_apply, one_ne_zero]

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