Documentation

Mathlib.Combinatorics.SimpleGraph.Acyclic

Acyclic graphs and trees #

This module introduces acyclic graphs (a.k.a. forests) and trees.

Main definitions #

Main statements #

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

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

Equations
  • G.IsAcyclic = ∀ ⦃v : V⦄ (c : G.Walk v v), ¬c.IsCycle
Instances For
    theorem SimpleGraph.isTree_iff {V : Type u} (G : SimpleGraph V) :
    G.IsTree G.Connected G.IsAcyclic
    structure SimpleGraph.IsTree {V : Type u} (G : SimpleGraph V) :

    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.

      @[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 wG.IsBridge s(v, w)
      theorem SimpleGraph.isAcyclic_iff_forall_edge_isBridge {V : Type u} {G : SimpleGraph V} :
      G.IsAcyclic ∀ ⦃e : Sym2 V⦄, e G.edgeSetG.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