compl — 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.\\mathrm{compl}.toGraph = h.toGraph^{\\complement}$$$

Lean4

/-- For `A : Matrix V V α`, `A.compl` is supposed to be the adjacency matrix of
the complement graph of the graph induced by `A.adjMatrix`. -/
def compl [Zero α] [One α] [DecidableEq α] [DecidableEq V] (A : Matrix V V α) : Matrix V V α := fun i j =>
  ite (i = j) 0 (ite (A i j = 0) 1 0)

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