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 [Chou1994].

Tags

acyclic graphs, trees

def SimpleGraph.IsAcyclic {V : Type u} (G : SimpleGraph V) : Prop

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

Equations

• G.IsAcyclic = ∀ ⦃v : V⦄ (c : G.Walk v v), ¬c.IsCycle

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

A tree is a connected acyclic graph.

• isConnected : G.Connected

  Graph is connected.

• IsAcyclic : G.IsAcyclic

  Graph is acyclic.

theorem SimpleGraph.isTree_iff {V : Type u} (G : SimpleGraph V) : G.IsTree ↔ G.Connected ∧ G.IsAcyclic

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.

@[simp]

theorem SimpleGraph.isAcyclic_bot {V : Type u} : ⊥.IsAcyclic

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_iff_forall_edge_isBridge {V : Type u} {G : SimpleGraph V} : G.IsAcyclic ↔ ∀ ⦃e : Sym2 V⦄, e ∈ G.edgeSet → G.IsBridge e

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

theorem SimpleGraph.isTree_iff_existsUnique_path {V : Type u} {G : SimpleGraph V} : G.IsTree ↔ Nonempty V ∧ ∀ (v w : V), ∃! p : G.Walk v w, p.IsPath

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