feat: Girth of a simple graph (#6948)

Define the girth of a simple graph as a `ℕ∞`.

Mathlib.lean

@@ -1256,6 +1256,7 @@ import Mathlib.Combinatorics.SimpleGraph.Density
 import Mathlib.Combinatorics.SimpleGraph.Ends.Defs
 import Mathlib.Combinatorics.SimpleGraph.Ends.Properties
 import Mathlib.Combinatorics.SimpleGraph.Finsubgraph
+import Mathlib.Combinatorics.SimpleGraph.Girth
 import Mathlib.Combinatorics.SimpleGraph.Hasse
 import Mathlib.Combinatorics.SimpleGraph.IncMatrix
 import Mathlib.Combinatorics.SimpleGraph.Init

Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

@@ -63,6 +63,8 @@ structure IsTree : Prop where
 
 variable {G}
 
+@[simp] lemma isAcyclic_bot : IsAcyclic (⊥ : SimpleGraph V) := λ _a _w hw ↦ hw.ne_bot rfl
+
 theorem isAcyclic_iff_forall_adj_isBridge :
     G.IsAcyclic ↔ ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge ⟦(v, w)⟧ := by
   simp_rw [isBridge_iff_adj_and_forall_cycle_not_mem]

Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

@@ -1082,6 +1082,10 @@ theorem IsPath.of_append_right {u v w : V} {p : G.Walk u v} {q : G.Walk v w}
 theorem IsCycle.not_of_nil {u : V} : ¬(nil : G.Walk u u).IsCycle := fun h => h.ne_nil rfl
 #align simple_graph.walk.is_cycle.not_of_nil SimpleGraph.Walk.IsCycle.not_of_nil
 
+lemma IsCycle.ne_bot : ∀ {p : G.Walk u u}, p.IsCycle → G ≠ ⊥
+| nil, hp => by cases hp.ne_nil rfl
+| cons h _, hp => by rintro rfl; exact h
+
 theorem cons_isCycle_iff {u v : V} (p : G.Walk v u) (h : G.Adj u v) :
     (Walk.cons h p).IsCycle ↔ p.IsPath ∧ ¬⟦(u, v)⟧ ∈ p.edges := by
   simp only [Walk.isCycle_def, Walk.isPath_def, Walk.isTrail_def, edges_cons, List.nodup_cons,

Mathlib/Combinatorics/SimpleGraph/Girth.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2023 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import Mathlib.Combinatorics.SimpleGraph.Acyclic
+import Mathlib.Data.ENat.Lattice
+
+/-!
+# 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.
+-/
+
+namespace SimpleGraph
+variable {α : Type*} {G : SimpleGraph α} {n : ℕ∞}
+
+/-- The girth of a simple graph is the length of its smallest cycle, or `∞` if the graph is acyclic.
+-/
+noncomputable def girth (G : SimpleGraph α) : ℕ∞ :=
+⨅ a, ⨅ w : G.Walk a a, ⨅ _ : w.IsCycle, w.length
+
+@[simp] lemma le_girth : n ≤ G.girth ↔ ∀ a (w : G.Walk a a), w.IsCycle → n ≤ w.length := by
+  simp [girth]
+
+@[simp] lemma girth_eq_top : G.girth = ⊤ ↔ G.IsAcyclic := by simp [girth, IsAcyclic]
+
+protected alias ⟨_, IsAcyclic.girth_eq_top⟩ := girth_eq_top
+
+lemma girth_anti : Antitone (girth : SimpleGraph α → ℕ∞) :=
+λ G H h ↦ iInf_mono λ a ↦ iInf₂_mono' λ w hw ↦ ⟨w.mapLe h, hw.mapLe _, by simp⟩
+
+lemma exists_girth_eq_length :
+  (∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.girth = w.length) ↔ ¬ G.IsAcyclic := by
+  refine' ⟨_, λ h ↦ _⟩
+  · rintro ⟨a, w, hw, _⟩ hG
+    exact hG _ hw
+  · simp_rw [←girth_eq_top, ←Ne.def, girth, iInf_subtype', iInf_sigma', ENat.iInf_coe_ne_top,
+      ←exists_prop, Subtype.exists', Sigma.exists', eq_comm] at h ⊢
+    exact ciInf_mem _
+
+@[simp] lemma girth_bot : girth (⊥ : SimpleGraph α) = ⊤ := by simp
+
+end SimpleGraph