Adjacency Matrices #
This module defines the adjacency matrix of a graph, and provides theorems connecting graph
properties to computational properties of the matrix.
Main definitions #
- zero_or_one : (∀ (i j : V), A i j = 0 ∨ A i j = 1) . "obviously"
- symm : A.is_symm . "obviously"
- apply_diag : (∀ (i : V), A i i = 0) . "obviously"
A : matrix V V α is qualified as an "adjacency matrix" if
(1) every entry of
A is symmetric,
(3) every diagonal entry of
A : matrix V V α and
h : is_adj_matrix A,
h.to_graph is the simple graph whose adjacency matrix is
A : matrix V V α,
A.compl is supposed to be the adjacency matrix of
the complement graph of the graph induced by
adj_matrix G α is the matrix
A such that
A i j = (1 : α) if
adjacent in the simple graph
G, and otherwise
A i j = 0.
The adjacency matrix of
G is an adjacency matrix.
The graph induced by the adjacency matrix of
A is qualified as an adjacency matrix,
then the adjacency matrix of the graph induced by
A is itself.