Commit 2025-03-28 02:52 96e12f2d

View on Github →

feat(Combinatorics/SimpleGraph/Diam): add basic (e)diam facts (#23264) Add converses of some diam and ediam lemmas. These should improve the experience of working with diam/ediam by providing more direct relations between the terms G.ediam = \top, G.diam = 0, G.Preconnected, etc.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Diam.lean

added theorem SimpleGraph.connected_iff_diam_ne_zero

added theorem SimpleGraph.connected_iff_ediam_ne_top

added theorem SimpleGraph.connected_of_ediam_ne_top

added theorem SimpleGraph.diam_eq_zero_iff_ediam_eq_top

added theorem SimpleGraph.diam_ne_zero_of_ediam_ne_top

added theorem SimpleGraph.preconnected_of_ediam_ne_top