toGraph_adjMatrix_eq — Mathlib

English

The graph induced by the adjacency matrix of G is G itself.

Русский

Граф, порождаемый матрицей смежности графа G, есть сам G.

LaTeX

$$(G.isAdjMatrix_adjMatrix α).toGraph = G$$

Lean4

/-- The graph induced by the adjacency matrix of `G` is `G` itself. -/
theorem toGraph_adjMatrix_eq [MulZeroOneClass α] [Nontrivial α] : (G.isAdjMatrix_adjMatrix α).toGraph = G :=
  by
  ext
  simp only [IsAdjMatrix.toGraph_adj, adjMatrix_apply, ite_eq_left_iff, zero_ne_one]
  apply Classical.not_not

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