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

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

@[simp]

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

@[simp]

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

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

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 : G.Walk a a), w.IsCycle ∧ G.girth = ↑w.length) ↔ ¬G.IsAcyclic

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

@[simp]

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