Acyclic graphs and trees #
This module introduces acyclic graphs (a.k.a. forests) and trees.
Main definitions #
SimpleGraph.IsAcyclic
is a predicate for a graph having no cyclic walksSimpleGraph.IsTree
is a predicate for a graph being a tree (a connected acyclic graph)
Main statements #
SimpleGraph.isAcyclic_iff_path_unique
characterizes acyclicity in terms of uniqueness of paths between pairs of vertices.SimpleGraph.isAcyclic_iff_forall_edge_isBridge
characterizes acyclicity in terms of every edge being a bridge edge.SimpleGraph.isTree_iff_existsUnique_path
characterizes trees in terms of existence and uniqueness of paths between pairs of vertices from a nonempty vertex type.
References #
The structure of the proofs for SimpleGraph.IsAcyclic
and SimpleGraph.IsTree
, including
supporting lemmas about SimpleGraph.IsBridge
, generally follows the high-level description
for these theorems for multigraphs from [Chou1994].
Tags #
acyclic graphs, trees
A graph is acyclic (or a forest) if it has no cycles.
Instances For
A tree is a connected acyclic graph.
- isConnected : G.Connected
Graph is connected.
- IsAcyclic : G.IsAcyclic
Graph is acyclic.
Instances For
theorem
SimpleGraph.IsTree.isConnected
{V : Type u}
{G : SimpleGraph V}
(self : G.IsTree)
:
G.Connected
Graph is connected.
theorem
SimpleGraph.IsTree.IsAcyclic
{V : Type u}
{G : SimpleGraph V}
(self : G.IsTree)
:
G.IsAcyclic
Graph is acyclic.
theorem
SimpleGraph.isAcyclic_iff_forall_adj_isBridge
{V : Type u}
{G : SimpleGraph V}
:
G.IsAcyclic ↔ ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)
theorem
SimpleGraph.IsAcyclic.path_unique
{V : Type u}
{G : SimpleGraph V}
(h : G.IsAcyclic)
{v : V}
{w : V}
(p : G.Path v w)
(q : G.Path v w)
:
p = q
theorem
SimpleGraph.isAcyclic_of_path_unique
{V : Type u}
{G : SimpleGraph V}
(h : ∀ (v w : V) (p q : G.Path v w), p = q)
:
G.IsAcyclic
theorem
SimpleGraph.IsTree.existsUnique_path
{V : Type u}
{G : SimpleGraph V}
(hG : G.IsTree)
(v : V)
(w : V)
:
∃! p : G.Walk v w, p.IsPath
theorem
SimpleGraph.IsTree.card_edgeFinset
{V : Type u}
{G : SimpleGraph V}
[Fintype V]
[Fintype ↑G.edgeSet]
(hG : G.IsTree)
:
G.edgeFinset.card + 1 = Fintype.card V