incMatrix_apply_eq_one_iff — Mathlib

English

Under the same hypotheses, the incidence-matrix entry G.incMatrix R a e equals one precisely when e belongs to the incidenceSet a.

Русский

При тех же условиях запись incMatrix R a e равна единице тогда, когда e принадлежит incindenceSet a.

LaTeX

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

Lean4

theorem incMatrix_apply_eq_one_iff : G.incMatrix R a e = 1 ↔ e ∈ G.incidenceSet a :=
  by
  convert one_ne_zero.ite_eq_left_iff
  infer_instance

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