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 walks.SimpleGraph.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 [Cho94].
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.
Instances For
A graph that has an injective homomorphism to an acyclic graph is acyclic.
Isomorphic graphs are acyclic together.
Isomorphic graphs are trees together.
A graph induced from an acyclic graph is acyclic.
A subgraph of an acyclic graph is acyclic.
A spanning subgraph of an acyclic graph is acyclic.
A connected component of an acyclic graph is a tree.
A minimally connected graph is a tree.
Every connected graph has a spanning tree.
Every connected graph on n
vertices has at least n-1
edges.
The minimum degree of all vertices in a nontrivial tree is one.
A nontrivial tree has a vertex of degree one.