Reachability and connectedness

TheoremParent vertex towards a root in a connected graph#✓fully proved

In a connected graph every vertex v ≠ s has a neighbor p one step closer to s (a parent of v in a breadth-first tree rooted at s).

theorem exists_parent {V : Type*} {G : SimpleGraph V} (hG : G.Connected) {s v : V}
    (hv : v ≠ s) : ∃ p, G.Adj v p ∧ G.dist s p + 1 = G.dist s v

Used by 3

Used byClusters of an unrooted tree form a binary hierarchy · Clusters determine an unrooted binary tree · Split set from any leaf equals the edge splits

DefinitionInternally disjoint walks#✓fully proved

Two walks \(p\) and \(q\) in a simple graph \(G\) are internally disjoint if no vertex is an interior vertex of both, where the interior vertices of a walk are the entries of its vertex sequence other than the first and the last.

def InternallyDisjoint {u v x y : V} (p : G.Walk u v) (q : G.Walk x y) : Prop :=
  Disjoint p.support.tail.dropLast q.support.tail.dropLast

Used by 1

Used byInfinitely connected graphs

DefinitionInfinitely connected graphs#✓fully proved

A simple graph \(G\) is infinitely connected if it has at least two vertices and, for any two distinct vertices \(u\) and \(v\), there is an infinite set of paths from \(u\) to \(v\) in \(G\) that are pairwise internally disjoint.

In particular, a graph with at most one vertex is not infinitely connected.

def InfinitelyConnected (G : SimpleGraph V) : Prop := Nontrivial V ∧
  Pairwise fun u v ↦ ∃ P : Set (G.Walk u v),
    P.Infinite ∧ (∀ p ∈ P, p.IsPath) ∧ P.Pairwise InternallyDisjoint

Uses 1

Statement usesInternally disjoint walks

DefinitionOne round of breadth-first search#✓fully proved

For a simple graph \(G\) on a finite vertex set and a set \(s\) of vertices, this is the set of vertices that lie in \(s\) or are adjacent to some vertex of \(s\), that is, \(s\) together with all neighbours of its vertices.

def bfsStep : Finset V := {w | w ∈ s ∨ ∃ v ∈ s, G.Adj v w}

Used by 1

Used byBreadth-first search with a round limit

DefinitionBreadth-first search with a round limit#✓fully proved

For a simple graph \(G\) on a finite vertex set, a natural number \(n\) and a set \(s\) of vertices, this applies rounds of breadth-first search to \(s\) (each round adds all neighbours of the current vertices), stopping after \(n\) rounds or as soon as a round adds no new vertex, whichever comes first, and returns the resulting set.

def bfsIterate : ℕ → Finset V → Finset V
  | 0, s => s
  | n + 1, s => if (G.bfsStep s).card ≤ s.card then s else bfsIterate n (G.bfsStep s)

Uses 1 · Used by 1

Statement usesOne round of breadth-first search

Used byVertices reachable from a vertex

DefinitionVertices reachable from a vertex#✓fully proved

For a simple graph \(G\) on a finite vertex set \(V\) and a vertex \(u\), this is the set obtained from \(\{u\}\) by breadth-first search with at most \(|V|\) rounds, stopping early as soon as a round adds no new vertex.

It consists exactly of the vertices reachable from \(u\) in \(G\).

def reachableFinset (u : V) : Finset V := G.bfsIterate (Fintype.card V) {u}

Uses 1

Statement usesBreadth-first search with a round limit

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.