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

## Tags #

acyclic graphs, trees

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

## Instances For

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

G.Connected

Graph is connected.

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

G.IsAcyclic

Graph is acyclic.

theorem
SimpleGraph.isAcyclic_iff_forall_adj_isBridge
{V : Type u}
{G : SimpleGraph V}
:

G.IsAcyclic ↔ ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w)

theorem
SimpleGraph.IsAcyclic.path_unique
{V : Type u}
{G : SimpleGraph V}
(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 : SimpleGraph V}
(h : ∀ (v w : V) (p q : G.Path v w), p = q)
:

G.IsAcyclic

theorem
SimpleGraph.IsTree.existsUnique_path
{V : Type u}
{G : SimpleGraph V}
(hG : G.IsTree)
(v : V)
(w : V)
:

∃! p : G.Walk v w, p.IsPath

theorem
SimpleGraph.IsTree.card_edgeFinset
{V : Type u}
{G : SimpleGraph V}
[Fintype V]
[Fintype ↑G.edgeSet]
(hG : G.IsTree)
:

G.edgeFinset.card + 1 = Fintype.card V