# mathlib3documentation

combinatorics.simple_graph.acyclic

# 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_acyclic is a predicate for a graph having no cyclic walks
• simple_graph.is_tree is a predicate for a graph being a tree (a connected acyclic graph)

## Main statements #

• simple_graph.is_acyclic_iff_path_unique characterizes acyclicity in terms of uniqueness of paths between pairs of vertices.
• simple_graph.is_acyclic_iff_forall_edge_is_bridge characterizes acyclicity in terms of every edge being a bridge edge.
• simple_graph.is_tree_iff_exists_unique_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 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

def simple_graph.is_acyclic {V : Type u} (G : simple_graph V) :
Prop

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

Equations
structure simple_graph.is_tree {V : Type u} (G : simple_graph V) :
Prop
• is_connected :
• is_acyclic :

A tree is a connected acyclic graph.

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
theorem simple_graph.is_tree_iff_exists_unique_path {V : Type u} {G : simple_graph V} :
G.is_tree (v w : V), ∃! (p : G.walk v w), p.is_path