# 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 [Chou1994].

## Tags #

acyclic graphs, trees

def SimpleGraph.IsAcyclic {V : Type u} (G : ) :

A graph is acyclic (or a forest) if it has no cycles.

Equations
• G.IsAcyclic = ∀ ⦃v : V⦄ (c : G.Walk v v), ¬c.IsCycle
Instances For
theorem SimpleGraph.isTree_iff {V : Type u} (G : ) :
G.IsTree G.Connected G.IsAcyclic
structure SimpleGraph.IsTree {V : Type u} (G : ) :

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 : } (self : G.IsTree) :
G.Connected

Graph is connected.

theorem SimpleGraph.IsTree.IsAcyclic {V : Type u} {G : } (self : G.IsTree) :
G.IsAcyclic

Graph is acyclic.

@[simp]
theorem SimpleGraph.isAcyclic_bot {V : Type u} :
.IsAcyclic
theorem SimpleGraph.isAcyclic_iff_forall_adj_isBridge {V : Type u} {G : } :
G.IsAcyclic ∀ ⦃v w : V⦄, G.Adj v wG.IsBridge s(v, w)
theorem SimpleGraph.isAcyclic_iff_forall_edge_isBridge {V : Type u} {G : } :
G.IsAcyclic ∀ ⦃e : Sym2 V⦄, e G.edgeSetG.IsBridge e
theorem SimpleGraph.IsAcyclic.path_unique {V : Type u} {G : } (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 : } (h : ∀ (v w : V) (p q : G.Path v w), p = q) :
G.IsAcyclic
theorem SimpleGraph.isAcyclic_iff_path_unique {V : Type u} {G : } :
G.IsAcyclic ∀ ⦃v w : V⦄ (p q : G.Path v w), p = q
theorem SimpleGraph.isTree_iff_existsUnique_path {V : Type u} {G : } :
G.IsTree ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath
theorem SimpleGraph.IsTree.existsUnique_path {V : Type u} {G : } (hG : G.IsTree) (v : V) (w : V) :
∃! p : G.Walk v w, p.IsPath
theorem SimpleGraph.IsTree.card_edgeFinset {V : Type u} {G : } [] [Fintype G.edgeSet] (hG : G.IsTree) :
G.edgeFinset.card + 1 =