diameter of a ball

Stream: Is there code for X?

[Ruben Van de Velde]

I found docs#Metric.diam_ball but this is an inequality. Am I wrong to expect that the equality holds (under appropriate conditions)?

[Alex J. Best]

There would be many examples where this fails for arbitrary (even complete) metric spaces, a quick google suggests that normed vector space is sufficient but I couldn't find that in mathlib

[Junyan Xu]

Maybe adapt the proof of docs#closure_ball

[Jireh Loreaux]

I think not too long ago @Alex Kontorovich was interested in the conditions under which the closure of any open ball is the corresponding closed ball, which is not exactly the same, but seems related, as Junyan Xu notes.

[Yaël Dillies]

This is more or less the same question, yes. It all depends on whether 1 is a limit point of d(x, y) when y ranges over all points.