Documentation

Mathlib.Combinatorics.SimpleGraph.Girth

Girth of a simple graph #

This file defines the girth and the extended girth of a simple graph as the length of its smallest cycle, they give 0 or ∞ respectively if the graph is acyclic.

source
noncomputable def SimpleGraph.egirth {α : Type u_1} (G : SimpleGraph α) :
ℕ∞

The extended girth of a simple graph is the length of its smallest cycle, or ∞ if the graph is acyclic.

Equations
  • G.egirth = ⨅ (a : α), ⨅ (w : G.Walk a a), ⨅ (_ : w.IsCycle), ↑w.length
Instances For
    source
    @[simp]
    theorem SimpleGraph.le_egirth {α : Type u_1} {G : SimpleGraph α} {n : ℕ∞} :
    n ≤ G.egirth ↔ ∀ (a : α) (w : G.Walk a a), w.IsCycle → n ≤ ↑w.length
    source
    @[simp]
    theorem SimpleGraph.egirth_eq_top {α : Type u_1} {G : SimpleGraph α} :
    G.egirth = ⊤ ↔ G.IsAcyclic
    source
    theorem SimpleGraph.IsAcyclic.egirth_eq_top {α : Type u_1} {G : SimpleGraph α} :
    G.IsAcyclic → G.egirth = ⊤

    Alias of the reverse direction of SimpleGraph.egirth_eq_top.

    source
    theorem SimpleGraph.egirth_anti {α : Type u_1} :
    Antitone SimpleGraph.egirth
    source
    theorem SimpleGraph.exists_egirth_eq_length {α : Type u_1} {G : SimpleGraph α} :
    (∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.egirth = ↑w.length) ↔ ¬G.IsAcyclic
    source
    theorem SimpleGraph.three_le_egirth {α : Type u_1} {G : SimpleGraph α} :
    3 ≤ G.egirth
    source
    @[simp]
    theorem SimpleGraph.egirth_bot {α : Type u_1} :
    ⊥.egirth = ⊤
    source
    noncomputable def SimpleGraph.girth {α : Type u_1} (G : SimpleGraph α) :
    ℕ

    The girth of a simple graph is the length of its smallest cycle, or junk value 0 if the graph is acyclic.

    Equations
    • G.girth = G.egirth.toNat
    Instances For
      source
      theorem SimpleGraph.three_le_girth {α : Type u_1} {G : SimpleGraph α} (hG : ¬G.IsAcyclic) :
      3 ≤ G.girth
      source
      theorem SimpleGraph.girth_eq_zero {α : Type u_1} {G : SimpleGraph α} :
      G.girth = 0 ↔ G.IsAcyclic
      source
      theorem SimpleGraph.IsAcyclic.girth_eq_zero {α : Type u_1} {G : SimpleGraph α} :
      G.IsAcyclic → G.girth = 0

      Alias of the reverse direction of SimpleGraph.girth_eq_zero.

      source
      theorem SimpleGraph.girth_anti {α : Type u_1} {G : SimpleGraph α} {G' : SimpleGraph α} (hab : G ≤ G') (h : ¬G.IsAcyclic) :
      G'.girth ≤ G.girth
      source
      theorem SimpleGraph.exists_girth_eq_length {α : Type u_1} {G : SimpleGraph α} :
      (∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.girth = w.length) ↔ ¬G.IsAcyclic
      source
      @[simp]
      theorem SimpleGraph.girth_bot {α : Type u_1} :
      ⊥.girth = 0