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 #
The structure of the proofs for
supporting lemmas about
simple_graph.is_bridge, generally follows the high-level description
for these theorems for multigraphs from [Cho94].
acyclic graphs, trees
A graph is acyclic (or a forest) if it has no cycles.
A tree is a connected acyclic graph.