Adjacency matrix

23 fully proved

Adjacency Matrix

StructureAdjacency matrix#✓fully proved

For a natural number \(n\), an adjacency matrix on \(n\) vertices is a directed graph on the vertex set \(\{0, \dots, n-1\}\) given by a Boolean-valued function \(\mathrm{adj}\) on ordered pairs of vertices: \(\mathrm{adj}(i, j)\) is true exactly when there is a directed edge from \(i\) to \(j\).

structure AdjacencyMatrix (n : Nat) where
  /-- `adj i j = true` when there is a directed edge from `i` to `j`. -/
  adj : Fin n → Fin n → Bool

Used by 19

Used byEdge insertion in an adjacency matrix · Empty adjacency matrix · Edge deletion in an adjacency matrix · Extensionality of adjacency matrices · Edge query of an adjacency matrix · An inserted edge is present · Edges after inserting an edge · Inserting an edge leaves other pairs unchanged · Deleting an edge removes it · Edges after deleting an edge · Deleting an edge leaves the other entries unchanged · The out-neighbor list matches the edge query · Adding an edge makes its target an out-neighbor · Out-neighbors after adding an edge · Out-neighbor list · Out-neighbor lists have no duplicates · Out-neighbor lists are strictly increasing · Deleting an edge removes the out-neighbor · Out-degree

DefinitionEmpty adjacency matrix#✓fully proved

For every natural number \(n\), the empty adjacency matrix on \(n\) vertices is the directed graph on \(\{0, \dots, n-1\}\) with no edges: its adjacency function is false on every ordered pair of vertices.

def empty {n : Nat} : AdjacencyMatrix n :=
  ⟨fun _ _ => false⟩

Uses 1 · Used by 3

Statement usesAdjacency matrix

Used byThe empty adjacency matrix has no edges · Out-neighbor lists of the empty graph · Vertices of the empty graph have out-degree zero

DefinitionEdge query of an adjacency matrix#✓fully proved

For an adjacency matrix \(m\) on the vertex set \(\{0, \dots, n-1\}\) and vertices \(i, j\), the edge query of \(m\) at \((i, j)\) is the Boolean value that is true exactly when \(m\) has a directed edge from \(i\) to \(j\).

def hasEdge {n : Nat} (m : AdjacencyMatrix n) (i j : Fin n) : Bool :=
  m.adj i j

Uses 1 · Used by 16

Statement usesAdjacency matrix

Used byExtensionality of adjacency matrices · An inserted edge is present · Edges after inserting an edge · Inserting an edge leaves other pairs unchanged · The empty adjacency matrix has no edges · Deleting an edge removes it · Edges after deleting an edge · Deleting an edge leaves the other entries unchanged · The out-neighbor list matches the edge query · Adding an edge makes its target an out-neighbor · Out-neighbors after adding an edge · Out-neighbor list · Out-neighbor lists of the empty graph · Out-neighbor lists have no duplicates · Out-neighbor lists are strictly increasing · Deleting an edge removes the out-neighbor

TheoremThe empty adjacency matrix has no edges#✓fully proved

For every natural number \(n\) and all vertices \(i\) and \(j\) among the \(n\) vertices, the empty adjacency matrix on \(n\) vertices has no edge from \(i\) to \(j\).

@[simp]
theorem hasEdge_empty {n : Nat} (i j : Fin n) :
    (empty : AdjacencyMatrix n).hasEdge i j = false

Uses 2

Statement usesEmpty adjacency matrix · Edge query of an adjacency matrix

DefinitionEdge insertion in an adjacency matrix#✓fully proved

For an adjacency matrix \(m\) on the vertex set \(\{0, \dots, n-1\}\) and vertices \(i\) and \(j\), adding the edge from \(i\) to \(j\) gives the adjacency matrix that has an edge from \(i\) to \(j\) and agrees with \(m\) on every other ordered pair of vertices.

def addEdge {n : Nat} (m : AdjacencyMatrix n) (i j : Fin n) : AdjacencyMatrix n :=
  ⟨fun a b => if a = i ∧ b = j then true else m.adj a b⟩

Uses 1 · Used by 5

Statement usesAdjacency matrix

Used byAn inserted edge is present · Edges after inserting an edge · Inserting an edge leaves other pairs unchanged · Adding an edge makes its target an out-neighbor · Out-neighbors after adding an edge

TheoremAn inserted edge is present#✓fully proved

For an adjacency matrix \(m\) on \(n\) vertices and vertices \(i\) and \(j\), the matrix obtained from \(m\) by adding the edge from \(i\) to \(j\) has an edge from \(i\) to \(j\).

@[simp]
theorem hasEdge_addEdge {n : Nat} (m : AdjacencyMatrix n) (i j : Fin n) :
    (m.addEdge i j).hasEdge i j = true

Uses 3 · Used by 1

Statement usesAdjacency matrix · Edge insertion in an adjacency matrix · Edge query of an adjacency matrix

Used byAdding an edge makes its target an out-neighbor

TheoremInserting an edge leaves other pairs unchanged#✓fully proved

For an adjacency matrix \(m\) on \(n\) vertices and vertices \(i\), \(j\), \(a\), \(b\) with \(a \ne i\) or \(b \ne j\), the matrix obtained from \(m\) by adding the edge from \(i\) to \(j\) has an edge from \(a\) to \(b\) if and only if \(m\) does.

theorem hasEdge_addEdge_of_ne {n : Nat} (m : AdjacencyMatrix n) (i j a b : Fin n)
    (h : a ≠ i ∨ b ≠ j) :
    (m.addEdge i j).hasEdge a b = m.hasEdge a b

Uses 3

Statement usesAdjacency matrix · Edge insertion in an adjacency matrix · Edge query of an adjacency matrix

TheoremEdges after inserting an edge#✓fully proved

For an adjacency matrix \(m\) on \(n\) vertices and vertices \(i\), \(j\), \(a\), \(b\), the matrix obtained from \(m\) by adding the edge from \(i\) to \(j\) has an edge from \(a\) to \(b\) if and only if \(a = i\) and \(b = j\), or \(m\) has an edge from \(a\) to \(b\).

theorem hasEdge_addEdge_iff {n : Nat} (m : AdjacencyMatrix n) (i j a b : Fin n) :
    (m.addEdge i j).hasEdge a b = true ↔
      (a = i ∧ b = j) ∨ m.hasEdge a b = true

Uses 3 · Used by 1

Statement usesAdjacency matrix · Edge insertion in an adjacency matrix · Edge query of an adjacency matrix

Used byOut-neighbors after adding an edge

DefinitionEdge deletion in an adjacency matrix#✓fully proved

For an adjacency matrix \(m\) on the vertex set \(\{0, \dots, n-1\}\) and vertices \(i\) and \(j\), removing the edge from \(i\) to \(j\) gives the adjacency matrix that has no edge from \(i\) to \(j\) and agrees with \(m\) on every other ordered pair of vertices.

def eraseEdge {n : Nat} (m : AdjacencyMatrix n) (i j : Fin n) : AdjacencyMatrix n :=
  ⟨fun a b => if a = i ∧ b = j then false else m.adj a b⟩

Uses 1 · Used by 4

Statement usesAdjacency matrix

Used byDeleting an edge removes it · Edges after deleting an edge · Deleting an edge leaves the other entries unchanged · Deleting an edge removes the out-neighbor

TheoremDeleting an edge removes it#✓fully proved

Let \(m\) be an adjacency matrix on the vertex set \(\{0, \dots, n-1\}\) and let \(i, j\) be vertices. Then the graph obtained from \(m\) by deleting the edge from \(i\) to \(j\) has no edge from \(i\) to \(j\).

@[simp]
theorem hasEdge_eraseEdge {n : Nat} (m : AdjacencyMatrix n) (i j : Fin n) :
    (m.eraseEdge i j).hasEdge i j = false

Uses 3 · Used by 2

Statement usesAdjacency matrix · Edge deletion in an adjacency matrix · Edge query of an adjacency matrix

Used byEdges after deleting an edge · Deleting an edge removes the out-neighbor

TheoremDeleting an edge leaves the other entries unchanged#✓fully proved

Let \(m\) be an adjacency matrix on the vertex set \(\{0, \dots, n-1\}\) and let \(i, j, a, b\) be vertices with \((a, b) \ne (i, j)\), that is, \(a \ne i\) or \(b \ne j\). Then the graph obtained from \(m\) by deleting the edge from \(i\) to \(j\) has an edge from \(a\) to \(b\) if and only if \(m\) has an edge from \(a\) to \(b\).

theorem hasEdge_eraseEdge_of_ne {n : Nat} (m : AdjacencyMatrix n) (i j a b : Fin n)
    (h : a ≠ i ∨ b ≠ j) :
    (m.eraseEdge i j).hasEdge a b = m.hasEdge a b

Uses 3 · Used by 1

Statement usesAdjacency matrix · Edge deletion in an adjacency matrix · Edge query of an adjacency matrix

Used byEdges after deleting an edge

TheoremEdges after deleting an edge#✓fully proved

For an adjacency matrix \(m\) on \(n\) vertices and vertices \(i\), \(j\), \(a\), \(b\), the matrix obtained from \(m\) by removing the edge from \(i\) to \(j\) has an edge from \(a\) to \(b\) if and only if \((a, b) \ne (i, j)\) and \(m\) has an edge from \(a\) to \(b\).

theorem hasEdge_eraseEdge_iff {n : Nat} (m : AdjacencyMatrix n) (i j a b : Fin n) :
    (m.eraseEdge i j).hasEdge a b = true ↔
      ¬(a = i ∧ b = j) ∧ m.hasEdge a b = true

Uses 5

Statement usesAdjacency matrix · Edge deletion in an adjacency matrix · Edge query of an adjacency matrix

Proof usesDeleting an edge removes it · Deleting an edge leaves the other entries unchanged

TheoremExtensionality of adjacency matrices#✓fully proved

Two adjacency matrices \(m\) and \(m'\) on the same \(n\) vertices are equal if, for all vertices \(i\) and \(j\), \(m\) has an edge from \(i\) to \(j\) exactly when \(m'\) does.

@[ext]
theorem ext {n : Nat} {m m' : AdjacencyMatrix n}
    (h : ∀ i j, m.hasEdge i j = m'.hasEdge i j) : m = m'

Uses 2

Statement usesAdjacency matrix · Edge query of an adjacency matrix

DefinitionOut-neighbor list#✓fully proved

For an adjacency matrix \(m\) on the vertex set \(\{0, \dots, n-1\}\) and a vertex \(i\), the out-neighbor list of \(i\) is the list of all vertices \(j\) such that \(m\) has a directed edge from \(i\) to \(j\), in increasing order.

def neighbors {n : Nat} (m : AdjacencyMatrix n) (i : Fin n) : List (Fin n) :=
  (List.finRange n).filter fun j => m.hasEdge i j

Uses 2 · Used by 9

Statement usesAdjacency matrix · Edge query of an adjacency matrix

Used byThe out-neighbor list matches the edge query · Adding an edge makes its target an out-neighbor · Out-neighbors after adding an edge · Out-neighbor lists of the empty graph · Out-neighbor lists have no duplicates · Out-neighbor lists are strictly increasing · Deleting an edge removes the out-neighbor · Out-degree · Vertices of the empty graph have out-degree zero

TheoremThe out-neighbor list matches the edge query#✓fully proved

Let \(m\) be an adjacency matrix on the vertex set \(\{0, \dots, n-1\}\) and let \(i, j\) be vertices. Then \(j\) belongs to the out-neighbor list of \(i\) if and only if \(m\) has a directed edge from \(i\) to \(j\).

@[simp]
theorem mem_neighbors {n : Nat} (m : AdjacencyMatrix n) (i j : Fin n) :
    j ∈ m.neighbors i ↔ m.hasEdge i j = true

Uses 3 · Used by 4

Statement usesAdjacency matrix · Edge query of an adjacency matrix · Out-neighbor list

Used byAdding an edge makes its target an out-neighbor · Out-neighbors after adding an edge · Out-neighbor lists of the empty graph · Deleting an edge removes the out-neighbor

TheoremOut-neighbor lists have no duplicates#✓fully proved

For an adjacency matrix \(m\) on the vertex set \(\{0, \dots, n-1\}\) and a vertex \(i\), no vertex occurs twice in the out-neighbor list of \(i\).

theorem neighbors_nodup {n : Nat} (m : AdjacencyMatrix n) (i : Fin n) :
    (m.neighbors i).Nodup

Uses 3

Statement usesAdjacency matrix · Out-neighbor list

Proof usesEdge query of an adjacency matrix

TheoremOut-neighbor lists are strictly increasing#✓fully proved

For an adjacency matrix \(m\) on the vertex set \(\{0, \dots, n-1\}\) and a vertex \(i\), the out-neighbor list of \(i\) is strictly increasing: every vertex in it is smaller than every vertex that comes after it.

theorem neighbors_pairwise_lt {n : Nat} (m : AdjacencyMatrix n) (i : Fin n) :
    List.Pairwise (· < ·) (m.neighbors i)

Uses 3

Statement usesAdjacency matrix · Out-neighbor list

Proof usesEdge query of an adjacency matrix

TheoremOut-neighbor lists of the empty graph#✓fully proved

In the graph with no edges on the vertex set \(\{0, \dots, n-1\}\), the out-neighbor list of every vertex \(i\) is the empty list.

@[simp]
theorem neighbors_empty {n : Nat} (i : Fin n) :
    (empty : AdjacencyMatrix n).neighbors i = []

Uses 4 · Used by 1

Statement usesEmpty adjacency matrix · Out-neighbor list

Proof usesEdge query of an adjacency matrix · The out-neighbor list matches the edge query

Used byVertices of the empty graph have out-degree zero

TheoremAdding an edge makes its target an out-neighbor#✓fully proved

Let \(m\) be an adjacency matrix on the vertex set \(\{0, \dots, n-1\}\) and let \(i, j\) be vertices. Then \(j\) belongs to the out-neighbor list of \(i\) in the graph obtained from \(m\) by adding the edge from \(i\) to \(j\).

theorem mem_neighbors_addEdge {n : Nat} (m : AdjacencyMatrix n) (i j : Fin n) :
    j ∈ (m.addEdge i j).neighbors i

Uses 6

Statement usesAdjacency matrix · Edge insertion in an adjacency matrix · Out-neighbor list

Proof usesEdge query of an adjacency matrix · An inserted edge is present · The out-neighbor list matches the edge query

TheoremDeleting an edge removes the out-neighbor#✓fully proved

Let \(G\) be a directed graph on the vertices \(0, \dots, n-1\), given by its adjacency matrix, and let \(i\) and \(j\) be vertices. After the edge from \(i\) to \(j\) is deleted from \(G\) (whether or not \(G\) had that edge), \(j\) is not an out-neighbor of \(i\).

theorem not_mem_neighbors_eraseEdge {n : Nat} (m : AdjacencyMatrix n) (i j : Fin n) :
    j ∉ (m.eraseEdge i j).neighbors i

Uses 6

Statement usesAdjacency matrix · Edge deletion in an adjacency matrix · Out-neighbor list

Proof usesEdge query of an adjacency matrix · Deleting an edge removes it · The out-neighbor list matches the edge query

TheoremOut-neighbors after adding an edge#✓fully proved

Let \(m\) be an adjacency matrix on the vertex set \(\{0, \dots, n-1\}\) and let \(i, j, b\) be vertices. Then \(b\) belongs to the out-neighbor list of \(i\) in the graph obtained from \(m\) by adding the edge from \(i\) to \(j\) if and only if \(b = j\) or \(b\) belongs to the out-neighbor list of \(i\) in \(m\).

theorem mem_neighbors_addEdge_iff {n : Nat} (m : AdjacencyMatrix n)
    (i j b : Fin n) :
    b ∈ (m.addEdge i j).neighbors i ↔ b = j ∨ b ∈ m.neighbors i

Uses 6

Statement usesAdjacency matrix · Edge insertion in an adjacency matrix · Out-neighbor list

Proof usesEdge query of an adjacency matrix · Edges after inserting an edge · The out-neighbor list matches the edge query

DefinitionOut-degree#✓fully proved

The out-degree of a vertex \(i\) of a directed graph given by an adjacency matrix is the number of its out-neighbors, that is, the number of vertices \(j\) such that there is an edge from \(i\) to \(j\).

def outDegree {n : Nat} (m : AdjacencyMatrix n) (i : Fin n) : Nat :=
  (m.neighbors i).length

Uses 2 · Used by 1

Statement usesAdjacency matrix · Out-neighbor list

Used byVertices of the empty graph have out-degree zero

TheoremVertices of the empty graph have out-degree zero#✓fully proved

For every \(n\), every vertex of the empty directed graph on the vertices \(0, \dots, n-1\) has out-degree \(0\).

@[simp]
theorem outDegree_empty {n : Nat} (i : Fin n) :
    (empty : AdjacencyMatrix n).outDegree i = 0

Uses 4

Statement usesEmpty adjacency matrix · Out-degree

Proof usesOut-neighbor list · Out-neighbor lists of the empty graph

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.