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

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

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

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

A tree is a connected acyclic graph.

• isConnected : SimpleGraph.Connected G

  Graph is connected.

• IsAcyclic : SimpleGraph.IsAcyclic G

  Graph is acyclic.

@[simp]

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

theorem SimpleGraph.isAcyclic_iff_forall_adj_isBridge {V : Type u} {G : SimpleGraph V} : SimpleGraph.IsAcyclic G ↔ ∀ ⦃v w : V⦄, G.Adj v w → SimpleGraph.IsBridge G s(v, w)

theorem SimpleGraph.isAcyclic_iff_forall_edge_isBridge {V : Type u} {G : SimpleGraph V} : SimpleGraph.IsAcyclic G ↔ ∀ ⦃e : Sym2 V⦄, e ∈ SimpleGraph.edgeSet G → SimpleGraph.IsBridge G e

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) : SimpleGraph.IsAcyclic G

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

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

theorem SimpleGraph.IsTree.existsUnique_path {V : Type u} {G : SimpleGraph V} (hG : SimpleGraph.IsTree G) (v : V) (w : V) : ∃! (p : SimpleGraph.Walk G v w), SimpleGraph.Walk.IsPath p

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