uniform, metric and coarse spaces

Stream: general

[Daniel Roca González]

I would like to define coarse spaces, as in https://en.wikipedia.org/wiki/Coarse_structure. As coarse structures are "dual" to uniform structures, I am looking at the definition of uniform structures and adapting it. My problem comes when proving that metric spaces are examples of coarse spaces. In mathlib, the definition of a metric structure actually extends the definition of a uniform structure, with the justification that every metric space gives has a canonical uniform structure. The same phenomenon happens with coarse spaces: am I supposed to edit the mathlib definition of metric spaces so that it also extends my coarse spaces, or what is the best way to go about this?

[Kevin Buzzard]

If you're just making this as part of a project to learn lean then don't worry about the metric space thing. The reason it's there with uniform spaces is a technical implementation issue to do with identifying products of metric spaces and products of topological spaces.

[Kevin Buzzard]

Unless products of coarse spaces start getting seriously used in mathlib we can probably live with the technical problems

[Daniel Roca González]

thank you, I was able to do it :)