English
Radius equals ediam if and only if there exists an e such that every vertex has eccentricity e.
Русский
Радиус равен эдияму тогда и только тогда существует e, для которого для каждой вершины eccent(u) = e.
LaTeX
$$$$ G.radius = G.ediam \iff \exists e:\mathrm{ENat}, \forall u:\alpha,\ G.eccent(u) = e. $$$$
Lean4
theorem radius_eq_ediam_iff [Nonempty α] : G.radius = G.ediam ↔ ∃ e, ∀ u, G.eccent u = e :=
by
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· use G.radius
intro u
exact le_antisymm (h ▸ eccent_le_ediam) radius_le_eccent
· obtain ⟨e, h⟩ := h
have ediam_eq : G.ediam = e := le_antisymm (iSup_le fun u ↦ (h u).le) ((h Classical.ofNonempty) ▸ eccent_le_ediam)
rw [ediam_eq]
exact le_antisymm ((h Classical.ofNonempty) ▸ radius_le_eccent) (le_iInf fun u ↦ (h u).ge)
