Acyclic graphs and trees #

This module introduces acyclic graphs (a.k.a. forests) and trees.

Main definitions #

Main statements #

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

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

Instances For
    structure SimpleGraph.IsTree {V : Type u} (G : SimpleGraph V) :

    A tree is a connected acyclic graph.

    Instances For
      theorem SimpleGraph.IsAcyclic.path_unique {V : Type u} {G : SimpleGraph V} (h : SimpleGraph.IsAcyclic G) {v : V} {w : V} (p : SimpleGraph.Path G v w) (q : SimpleGraph.Path G v w) :
      p = q
      theorem SimpleGraph.isAcyclic_of_path_unique {V : Type u} {G : SimpleGraph V} (h : ∀ (v w : V) (p q : SimpleGraph.Path G v w), p = q) :
      theorem SimpleGraph.isAcyclic_iff_path_unique {V : Type u} {G : SimpleGraph V} :
      SimpleGraph.IsAcyclic G ∀ ⦃v w : V⦄ (p q : SimpleGraph.Path G v w), p = q