Acyclic graphs and trees #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This module introduces acyclic graphs (a.k.a. forests) and trees.
Main definitions #
simple_graph.is_acyclicis a predicate for a graph having no cyclic walkssimple_graph.is_treeis a predicate for a graph being a tree (a connected acyclic graph)
Main statements #
simple_graph.is_acyclic_iff_path_uniquecharacterizes acyclicity in terms of uniqueness of paths between pairs of vertices.simple_graph.is_acyclic_iff_forall_edge_is_bridgecharacterizes acyclicity in terms of every edge being a bridge edge.simple_graph.is_tree_iff_exists_unique_pathcharacterizes 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 simple_graph.is_acyclic and simple_graph.is_tree, including
supporting lemmas about simple_graph.is_bridge, 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.
theorem
simple_graph.is_tree_iff
{V : Type u}
(G : simple_graph V) :
G.is_tree ↔ G.connected ∧ G.is_acyclic
- is_connected : G.connected
- is_acyclic : G.is_acyclic
A tree is a connected acyclic graph.
theorem
simple_graph.is_acyclic_iff_forall_edge_is_bridge
{V : Type u}
{G : simple_graph V} :
G.is_acyclic ↔ ∀ ⦃e : sym2 V⦄, e ∈ ⇑simple_graph.edge_set G → G.is_bridge e
theorem
simple_graph.is_acyclic.path_unique
{V : Type u}
{G : simple_graph V}
(h : G.is_acyclic)
{v w : V}
(p q : G.path v w) :
p = q
theorem
simple_graph.is_acyclic_of_path_unique
{V : Type u}
{G : simple_graph V}
(h : ∀ (v w : V) (p q : G.path v w), p = q) :
theorem
simple_graph.is_acyclic_iff_path_unique
{V : Type u}
{G : simple_graph V} :
G.is_acyclic ↔ ∀ ⦃v w : V⦄ (p q : G.path v w), p = q