English
Let A be a matrix and h be an IsAdjMatrix A. Then h.toGraph is the simple graph on the vertex set V whose adjacency relation is given by i ~ j if and only if A i j = 1.
Русский
Пусть A — матрица, и h удовлетворяет условию IsAdjMatrix A. Тогда h.toGraph образует простой граф на множестве вершин V, у которого отношение смежности i ~ j задаётся как A i j = 1.
LaTeX
$$$\\\\forall i,j \in V,\\\\ h.toGraph.Adj(i,j) \iff A(i,j)=1$$$
Lean4
/-- For `A : Matrix V V α` and `h : IsAdjMatrix A`,
`h.toGraph` is the simple graph whose adjacency matrix is `A`. -/
@[simps]
def toGraph [MulZeroOneClass α] [Nontrivial α] (h : IsAdjMatrix A) : SimpleGraph V
where
Adj i j := A i j = 1
symm i j hij := by simp only; rwa [h.symm.apply i j]
loopless i := by simp [h]
