adjMatrix — Mathlib

English

The graph obtained by interpreting A.compl as an adjacency matrix is the complement of the graph obtained from A.

Русский

Граф, полученный из A.compl на основе матрицы смежности, является комплементом графа, полученного из A.

LaTeX

$$$h.compl.toGraph = h.toGraph^{\\complement}$$$

Lean4

/-- `adjMatrix G α` is the matrix `A` such that `A i j = (1 : α)` if `i` and `j` are
  adjacent in the simple graph `G`, and otherwise `A i j = 0`. -/
def adjMatrix [Zero α] [One α] : Matrix V V α :=
  of fun i j =>
    if G.Adj i j then (1 : α)
    else
      0
        -- TODO: set as an equation lemma for `adjMatrix`, see https://github.com/leanprover-community/mathlib4/pull/3024

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