Zulip Chat Archive

Stream: new members

Topic: Metric space distance has value in R?

Rémi Bottinelli (Feb 18 2022 at 05:47):

Hey! Is there a reason that the distance function on (pseudo) metric spaces isn't t\Rge0-valued?

Adam Topaz (Feb 18 2022 at 05:52):

It's actually both. Take a look at the definition of docs#pseudo_metric_space

Rémi Bottinelli (Feb 18 2022 at 05:53):

pseudo metric extends pseudo emetric, hence inherits the edist, and adds a dist ?

Kevin Buzzard (Feb 18 2022 at 08:51):

I think the reason is simply that ℝ is easier to use (eg it has a non-pathological subtraction)

Sebastien Gouezel (Feb 18 2022 at 09:19):

We have the function nndist which is nnreal-valued.

Eric Wieser (Feb 18 2022 at 09:32):


Last updated: Dec 20 2023 at 11:08 UTC