apply_ne_zero_iff — Mathlib

English

For an adjacency matrix of a simple graph, A_{ij} ≠ 0 iff A_{ij} = 1.

Русский

Для матрицы смежности простого графа A_{ij} ≠ 0 эквивалентно A_{ij} = 1.

LaTeX

$$$A.IsAdjMatrix \Rightarrow \forall i j, A_{ij} \neq 0 \iff A_{ij} = 1$$$

Lean4

@[simp]
theorem apply_ne_zero_iff [MulZeroOneClass α] [Nontrivial α] (h : IsAdjMatrix A) (i j : V) : ¬A i j = 0 ↔ A i j = 1 :=
  by rw [← apply_ne_one_iff h, Classical.not_not]

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