Wrenna Robson

See discussion here: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Opposite.20of.20diameter.20of.20an.20.28e.29metric.20space.2E

#12010 is relevant.

> LGTM, thanks! You can merge it once CI is happy. bors d+ Brilliant, thank you.

bors r+

I feel a bit stupid because I've written versions of this same file a bunch of times in the last few months, I never submitted it, and now you actually...

I would be interested to see if you could base this off my `infsep` branch. That construction was intended for use in a PR like this - it was held...

Note that I haven't changed any proofs unless strictly necessary - in one place (`floor_mono'`) I have added a lemma where there was an obvious loosening of both conclusion and...

Cool - I wonder if some sort of poll is appropriate to get a sense of community opinion on this? I can see both cases.

This PR actually does remove the TODO already, @ericrbg!

My understanding is that @YaelDillies wants to actually see the example that was cited - but there's no reason it has to be Yael who gives the OK here; that's...