SimpleGraph.IsAcyclic.girth_eq_top

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

This theorem, `SimpleGraph.IsAcyclic.girth_eq_top`, states that for any type `α` and any simple graph `G` of type `α`, if `G` is acyclic (meaning it has no cycles), then the girth of `G` (the length of the smallest cycle in `G`) is infinity (`⊤`). In simple terms, it says that an acyclic graph has an infinite girth, which makes sense as there are no cycles in such a graph.

More concisely: If `G` is a simple graph of type `α` with no cycles, then the girth of `G` is infinity.