Dropping uniformity

Stream: general

[Anatole Dedecker]

I've been working with uniform spaces quite a lot recently, and one really annoying thing that keeps coming over and over is that we have to used forms for talking about the uniformity filter :

• docs#uniformity, with the nice notation 𝓤
• uniform_space.to_core.uniformity, which quite a lot of lemmas are written for (see e.g docs#inf_uniformity, I introduced the primed version recently to use 𝓤), and more importantly, keeps coming over because using ext turns equalities of uniform spaces to equalities of their uniform_space.to_core.uniformity

I see too main options to fix that. The easy one is to declare that uniform_space.to_core.uniformity is an implementation detail, change all the lemmas to use docs#uniformity, including the @[ext] lemma docs#uniform_space_eq.

The more extreme solution would be to just remove docs#uniformity and use the nice notation for uniform_space.to_core.uniformity. I did that just for the basic file in draft PR #14694 if you want to have a look. Here are some pros and cons for this solution :

• pro : all the current uses of the notation seem to continue working flawlessly
• pro : when then uniform_space needs to be explicit, one can use u.uniformity instead of @uniformity _ u, but unfortunately
• con : due to the usual problems of dot notation, when writing u.uniformity, an extra type annotation is often needed, like (u : uniform_space α).uniformity. That said, I do prefer type annotation over @s and _s, but that's a personal preference
• con : the nice notation does not appear in the infoview (I guess this is because it's a "complicated" definition, in that it doesn't correspond to just one simple function application ?)

There might also be a solution involving abbreviation or reducible definitions, but I'm not familiar enough with this kind of things yet, so if you have any suggestion please let me know !

[Anatole Dedecker]

/poll Which option do you prefer ?
Make uniformity the preferred form, hide uniform_space.to_core.uniformity
Remove uniformity and assign notation to uniform_space.to_core.uniformity

[Anatole Dedecker]

cc @Patrick Massot @Sebastien Gouezel @Yury G. Kudryashov @Eric Wieser

[Yury G. Kudryashov]

You can introduce a notation like 𝓤[u] α similar to measurable_set[m] s.

[Yury G. Kudryashov]

(this applies to both solutions)

[Eric Wieser]

I think my comment on your PR fixes the second con

[Yury G. Kudryashov]

I have no opinion about your original question but I think that the user visible notation in the source files should be 𝓤 α and 𝓤[u] α. I'm not sure if we can use the latter notation in docs/infoview/...

[Patrick Massot]

I think it's nice to keep the notation in the info view. And uniform_space.to_core.uniformity is indeed an implementation detail.