apply_ne_one_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem apply_ne_one_iff [MulZeroOneClass α] [Nontrivial α] (h : IsAdjMatrix A) (i j : V) : ¬A i j = 1 ↔ A i j = 0 := by
  obtain h | h := h.zero_or_one i j <;> simp [h]

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