Girth of a simple graph

This file defines the girth of a simple graph as the length of its smallest cycle, or ∞ if the graph is acyclic.

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

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

Equations

• SimpleGraph.girth G = ⨅ (a : α), ⨅ (w : SimpleGraph.Walk G a a), ⨅ (_ : SimpleGraph.Walk.IsCycle w), ↑(SimpleGraph.Walk.length w)

@[simp]

theorem SimpleGraph.le_girth {α : Type u_1} {G : SimpleGraph α} {n : ℕ∞} : n ≤ SimpleGraph.girth G ↔ ∀ (a : α) (w : SimpleGraph.Walk G a a), SimpleGraph.Walk.IsCycle w → n ≤ ↑(SimpleGraph.Walk.length w)

@[simp]

theorem SimpleGraph.girth_eq_top {α : Type u_1} {G : SimpleGraph α} : SimpleGraph.girth G = ⊤ ↔ SimpleGraph.IsAcyclic G

theorem SimpleGraph.IsAcyclic.girth_eq_top {α : Type u_1} {G : SimpleGraph α} : SimpleGraph.IsAcyclic G → SimpleGraph.girth G = ⊤

Alias of the reverse direction of SimpleGraph.girth_eq_top.

theorem SimpleGraph.girth_anti {α : Type u_1} : Antitone SimpleGraph.girth

theorem SimpleGraph.exists_girth_eq_length {α : Type u_1} {G : SimpleGraph α} : (∃ (a : α) (w : SimpleGraph.Walk G a a), SimpleGraph.Walk.IsCycle w ∧ SimpleGraph.girth G = ↑(SimpleGraph.Walk.length w)) ↔ ¬SimpleGraph.IsAcyclic G

theorem SimpleGraph.three_le_girth {α : Type u_1} {G : SimpleGraph α} : 3 ≤ SimpleGraph.girth G

@[simp]

theorem SimpleGraph.girth_bot {α : Type u_1} : SimpleGraph.girth ⊥ = ⊤