# 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.

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

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
@[simp]
theorem SimpleGraph.le_egirth {α : Type u_1} {G : } {n : ℕ∞} :
n G.egirth ∀ (a : α) (w : G.Walk a a), w.IsCyclen w.length
@[simp]
theorem SimpleGraph.egirth_eq_top {α : Type u_1} {G : } :
G.egirth = G.IsAcyclic
theorem SimpleGraph.IsAcyclic.egirth_eq_top {α : Type u_1} {G : } :
G.IsAcyclicG.egirth =

Alias of the reverse direction of SimpleGraph.egirth_eq_top.

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

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
theorem SimpleGraph.three_le_girth {α : Type u_1} {G : } (hG : ¬G.IsAcyclic) :
3 G.girth
theorem SimpleGraph.girth_eq_zero {α : Type u_1} {G : } :
G.girth = 0 G.IsAcyclic
theorem SimpleGraph.IsAcyclic.girth_eq_zero {α : Type u_1} {G : } :
G.IsAcyclicG.girth = 0

Alias of the reverse direction of SimpleGraph.girth_eq_zero.

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