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_1} (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_1} (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_1} (G : SimpleGraph V) : G.IsTree ↔ G.Connected ∧ G.IsAcyclic

@[simp]

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

theorem SimpleGraph.IsAcyclic.comap {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') (hinj : Function.Injective ⇑f) (h : G'.IsAcyclic) : G.IsAcyclic

A graph that has an injective homomorphism to an acyclic graph is acyclic.

theorem SimpleGraph.IsAcyclic.embedding {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ↪g G') (h : G'.IsAcyclic) : G.IsAcyclic

theorem SimpleGraph.Iso.isAcyclic_iff {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ≃g G') : G.IsAcyclic ↔ G'.IsAcyclic

Isomorphic graphs are acyclic together.

theorem SimpleGraph.Iso.isTree_iff {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ≃g G') : G.IsTree ↔ G'.IsTree

Isomorphic graphs are trees together.

theorem SimpleGraph.IsAcyclic.of_map {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} (f : V ↪ V') (h : (SimpleGraph.map f G).IsAcyclic) : G.IsAcyclic

theorem SimpleGraph.IsAcyclic.of_comap {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} (f : V' ↪ V) (h : G.IsAcyclic) : (SimpleGraph.comap (⇑f) G).IsAcyclic

theorem SimpleGraph.IsAcyclic.induce {V : Type u_1} {G : SimpleGraph V} (h : G.IsAcyclic) (s : Set V) : (SimpleGraph.induce s G).IsAcyclic

A graph induced from an acyclic graph is acyclic.

theorem SimpleGraph.IsAcyclic.subgraph {V : Type u_1} {G : SimpleGraph V} (h : G.IsAcyclic) (H : G.Subgraph) : H.coe.IsAcyclic

A subgraph of an acyclic graph is acyclic.

theorem SimpleGraph.IsAcyclic.anti {V : Type u_1} {G G' : SimpleGraph V} (hsub : G ≤ G') (h : G'.IsAcyclic) : G.IsAcyclic

A spanning subgraph of an acyclic graph is acyclic.

theorem SimpleGraph.IsAcyclic.isTree_connectedComponent {V : Type u_1} {G : SimpleGraph V} (h : G.IsAcyclic) (c : G.ConnectedComponent) : c.toSimpleGraph.IsTree

A connected component of an acyclic graph is a tree.

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

theorem SimpleGraph.IsAcyclic.path_unique {V : Type u_1} {G : SimpleGraph V} (h : G.IsAcyclic) {v w : V} (p q : G.Path v w) : p = q

theorem SimpleGraph.isAcyclic_of_path_unique {V : Type u_1} {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_1} {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_1} {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_1} {G : SimpleGraph V} (hG : G.IsTree) (v w : V) : ∃! p : G.Walk v w, p.IsPath

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

theorem SimpleGraph.isTree_of_minimal_connected {V : Type u_1} {G : SimpleGraph V} (h : Minimal Connected G) : G.IsTree

A minimally connected graph is a tree.

theorem SimpleGraph.isTree_iff_minimal_connected {V : Type u_1} {G : SimpleGraph V} : G.IsTree ↔ Minimal Connected G

theorem SimpleGraph.Connected.exists_isTree_le {V : Type u_1} {G : SimpleGraph V} [Finite V] (h : G.Connected) : ∃ T ≤ G, T.IsTree

Every connected graph has a spanning tree.

theorem SimpleGraph.Connected.card_vert_le_card_edgeSet_add_one {V : Type u_1} {G : SimpleGraph V} (h : G.Connected) : Nat.card V ≤ Nat.card ↑G.edgeSet + 1

Every connected graph on n vertices has at least n-1 edges.

theorem SimpleGraph.isTree_iff_connected_and_card {V : Type u_1} {G : SimpleGraph V} [Finite V] : G.IsTree ↔ G.Connected ∧ Nat.card ↑G.edgeSet + 1 = Nat.card V

theorem SimpleGraph.IsTree.minDegree_eq_one_of_nontrivial {V : Type u_1} {G : SimpleGraph V} (h : G.IsTree) [Fintype V] [Nontrivial V] [DecidableRel G.Adj] : G.minDegree = 1

The minimum degree of all vertices in a nontrivial tree is one.

theorem SimpleGraph.IsTree.exists_vert_degree_one_of_nontrivial {V : Type u_1} {G : SimpleGraph V} [Fintype V] [Nontrivial V] [DecidableRel G.Adj] (h : G.IsTree) : ∃ (v : V), G.degree v = 1

A nontrivial tree has a vertex of degree one.