docs#metric.diam vs docs#emetric.diam

Stream: maths

[Yaël Dillies]

I'm a bit confused by metric.diam and emetric.diam. It sounds like one of them is meant to be for metric spaces and the other one for emetric spaces, but sets in metric spaces can also have infinite diameter! The real difference is between bounded and unbounded sets.

[Yaël Dillies]

Would it make more sense to rename metric.diam/emetric.diam to possibly_some_namespace.diam/possibly_some_namespace.ediam and possibly generalize typeclass assumptions on diam?

[Sebastien Gouezel]

diam takes its values in real numbers, just like the distance in metric spaces (and it is the supremum of dist x y for x and y in the set), while emetric.diam takes its values in ennreal, just like the distance in emetric spaces. (and it is the supremum of edist x y for x and y in the set). Can you explain again what you find confusing here?

[Yaël Dillies]

metric.diam is a concept about bounded sets and emetric.diam is a concept about all sets. There's no connection between the distance being emetric and boundedness of sets.

[Yaël Dillies]

I see why someone would do the analogy, but the analogy is wrong.

[Yaël Dillies]

I also note that emetric.diam is already called ediam in some (most?) lemma names, so at any rate it wouldn't be much work to change.

[Wrenna Robson]

Analogously to the shiny new set.infsep and set.einfsep, which is merging very soon, you could change them to set.diam and set.ediam. (Obviously for unbounded sets, set.diam makes less sense, but there are still things that will be true about it.)

[Wrenna Robson]

Which would indeed generalise the typeclass assumptions. I agree basically.

[Wrenna Robson]

(Also iirc diam is not the supremum by definition: that will need more typeclass or set assumptions to be true, basing it off infsep.)