total metric spaces

[malarbol]

Some work on total metric spaces: metric spaces such that all elements are at bounded distance.
I think it's related to distance functions:

• the existence of a distance function will make a metric space total;
• maybe there's some kind of converse, where we can use the inhabitedness of the set of upper bound on the distance to define some (lower|upper|)real that would effectively act as a distance?

I think we'll need this as an hypothesis for Banach fixed point theorem (or at least, the proof I have in mind uses it) so that's certainly a concept we might want to add at some point.

[lowasser]

We can define an upper real that acts as a distance; if we want to get it into a conventional real number I'm uncertain what conditions are required. I'd expect at least the need for decidability of the premetric.

[fredrik-bakke]

We can define an upper real that acts as a distance; if we want to get it into a conventional real number I'm uncertain what conditions are required. I'd expect at least the need for decidability of the premetric.

In case you weren't aware of this resource, here's a paper that considers some arithmetic on real numbers using upper and lower reals. It might have some answers for you, but I don't recall the details

https://www.researchgate.net/publication/362446739_Point-free_Construction_of_Real_Exponentiation
(Someone posted about it in #analysis in the Discord a short while ago)