adjMatrix_toGraph_eq — Mathlib

English

If A is the adjacency matrix of a graph, then the adjacency matrix of the graph induced by A is exactly A.

Русский

Пусть A является матрицей смежности графа; тогда матрица смежности графа, порождаемого A, равна A.

LaTeX

$$$h.toGraph.adjMatrix \alpha = A$$$

Lean4

/-- If `A` is qualified as an adjacency matrix,
then the adjacency matrix of the graph induced by `A` is itself. -/
theorem adjMatrix_toGraph_eq [DecidableEq α] : h.toGraph.adjMatrix α = A :=
  by
  ext i j
  obtain h' | h' := h.zero_or_one i j <;> simp [h']

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