toGraph_compl_eq — Mathlib

English

The graph induced by the complement of the adjacency matrix equals the complement of the original graph.

Русский

Граф, порожденный комплементом матрицы смежности, равен комплементу исходного графа.

LaTeX

$$$h.toGraph^{\\complement} = (h.toGraph)^{\\mathsf{c}}$$$

Lean4

theorem toGraph_compl_eq [MulZeroOneClass α] [Nontrivial α] (h : IsAdjMatrix A) : h.compl.toGraph = h.toGraphᶜ :=
  by
  ext v w
  rcases h.zero_or_one v w with h | h <;> by_cases hvw : v = w <;> simp [Matrix.compl, h, hvw]

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