cobounded vs cocompact

Stream: mathlib4

[Yury G. Kudryashov]

I'm adding more lemmas about docs#Bornology.cobounded. In particular, I'm going to replace all comap (dist c) atTop with cobounded _.

[Yury G. Kudryashov]

One of the lemmas says that in a proper metric space, cobounded X = cocompact X.

[Yury G. Kudryashov]

Should it be a simp lemma? If yes, in which direction?

[Kevin Buzzard]

If you're not sure which way then is this evidence it should just be left and we can wait for someone else to tag it later? Or is it important to know now so you know which way round to write it?

[Anatole Dedecker]

I don’t think this should be a simp lemma, I feel like it would be more annoying than useful

[Yury G. Kudryashov]

The main argument for making this a simp lemma is that we should have one canonical way to speak about this filter on, e.g., docs#Complex.