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 : 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

@[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

theorem SimpleGraph.Walk.IsCycle.egirth_le_length {α : Type u_1} {G : SimpleGraph α} {a : α} {w : G.Walk a a} (h : w.IsCycle) : G.egirth ≤ ↑w.length

@[deprecated SimpleGraph.Walk.IsCycle.egirth_le_length (since := "2026-07-05")]

theorem SimpleGraph.egirth_le_length {α : Type u_1} {G : SimpleGraph α} {a : α} {w : G.Walk a a} (h : w.IsCycle) : G.egirth ≤ ↑w.length

Alias of SimpleGraph.Walk.IsCycle.egirth_le_length.

theorem SimpleGraph.Walk.IsCircuit.egirth_le_length {α : Type u_1} {G : SimpleGraph α} {a : α} {w : G.Walk a a} (hwc : w.IsCircuit) : G.egirth ≤ ↑w.length

@[simp]

theorem SimpleGraph.egirth_eq_top {α : Type u_1} {G : SimpleGraph α} : G.egirth = ⊤ ↔ G.IsAcyclic

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.

theorem SimpleGraph.egirth_anti {α : Type u_1} : Antitone egirth

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

theorem SimpleGraph.three_le_egirth {α : Type u_1} {G : SimpleGraph α} : 3 ≤ G.egirth

@[simp]

theorem SimpleGraph.egirth_bot {α : Type u_1} : ⊥.egirth = ⊤

theorem SimpleGraph.egirth_top {α : Type u_1} (h : 3 ≤ ENat.card α) : ⊤.egirth = 3

theorem SimpleGraph.egirth_le_two_mul_ediam_add_one {α : Type u_1} {G : SimpleGraph α} (h : ¬G.IsAcyclic) : G.egirth ≤ 2 * G.ediam + 1

theorem SimpleGraph.IsContained.egirth_le {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {G' : SimpleGraph β} (h : G.IsContained G') : G'.egirth ≤ G.egirth

theorem SimpleGraph.Iso.egirth_eq {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {G' : SimpleGraph β} (f : G ≃g G') : G.egirth = G'.egirth

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

theorem SimpleGraph.Walk.IsCycle.girth_le_length {α : Type u_1} {G : SimpleGraph α} {a : α} {w : G.Walk a a} (h : w.IsCycle) : G.girth ≤ w.length

@[deprecated SimpleGraph.Walk.IsCycle.girth_le_length (since := "2026-07-05")]

theorem SimpleGraph.girth_le_length {α : Type u_1} {G : SimpleGraph α} {a : α} {w : G.Walk a a} (h : w.IsCycle) : G.girth ≤ w.length

Alias of SimpleGraph.Walk.IsCycle.girth_le_length.

theorem SimpleGraph.natCast_girth_le_egirth {α : Type u_1} {G : SimpleGraph α} : ↑G.girth ≤ G.egirth

theorem SimpleGraph.three_le_girth {α : Type u_1} {G : SimpleGraph α} (hG : ¬G.IsAcyclic) : 3 ≤ G.girth

theorem SimpleGraph.girth_eq_zero {α : Type u_1} {G : SimpleGraph α} : G.girth = 0 ↔ G.IsAcyclic

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.

theorem SimpleGraph.girth_anti {α : Type u_1} {G G' : SimpleGraph α} (hab : G ≤ G') (h : ¬G.IsAcyclic) : G'.girth ≤ G.girth

theorem SimpleGraph.Walk.IsCircuit.girth_le_length {α : Type u_1} {G : SimpleGraph α} {a : α} {w : G.Walk a a} (hwc : w.IsCircuit) : G.girth ≤ w.length

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.girth_le_two_mul_ediam_add_one {α : Type u_1} {G : SimpleGraph α} : ↑G.girth ≤ 2 * G.ediam + 1

theorem SimpleGraph.girth_le_two_mul_diam_add_one {α : Type u_1} {G : SimpleGraph α} (h : G.ediam ≠ ⊤) : G.girth ≤ 2 * G.diam + 1

@[simp]

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

theorem SimpleGraph.girth_top {α : Type u_1} (h : 3 ≤ ENat.card α) : ⊤.girth = 3

theorem SimpleGraph.IsContained.girth_le {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {G' : SimpleGraph β} (h : G.IsContained G') (hG : ¬G.IsAcyclic) : G'.girth ≤ G.girth

theorem SimpleGraph.Iso.girth_eq {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {G' : SimpleGraph β} (f : G ≃g G') : G.girth = G'.girth