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.

TODO

• Prove that G.egirth ≤ 2 * G.ediam + 1 and G.girth ≤ 2 * G.diam + 1 when the diameter is non-zero.

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.egirth_le_length {α : Type u_1} {G : SimpleGraph α} {a : α} {w : G.Walk a a} (h : w.IsCycle) : 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.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.girth_le_length {α : Type u_1} {G : SimpleGraph α} {a : α} {w : G.Walk a a} (h : w.IsCycle) : G.girth ≤ w.length

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.exists_girth_eq_length {α : Type u_1} {G : SimpleGraph α} : (∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.girth = w.length) ↔ ¬G.IsAcyclic

@[simp]

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

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