mathlib3 documentation


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 #

Main statements #

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) :

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

structure simple_graph.is_tree {V : Type u} (G : simple_graph V) :

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