Theorem SimpleGraph.ediam_eq_top_iff_radius_eq_top

Modification history

2026-02-26 22:22

Mathlib/Combinatorics/SimpleGraph/Diam.lean

feat(Combinatorics/SimpleGraph/Diam): drop `Finite α` from `ediam_le_two_mul_radius` (#33764)

Added SimpleGraph.ediam_eq_top_iff_radius_eq_top View on Github →