uniformity

Stream: maths

[Patrick Massot]

@Johannes Hölzl The next thing we discussed in Amsterdam was def uniformity {α : Type*} [uniform_space α] : filter (α × α) := (@uniform_space.to_core α _).uniformity. There are a lot of places where we see @uniformity α _ but also a lot of place where α is indeed inferred. @Mario Carneiro seemed to think we should make α an explicit argument in this definition. This is not an easy decision. Simply changing the argument type results in a lot or errors in uniform_space.basic. So I won't PR this change before discussing it more. My opinion is we should change it anyway, because I find many statements and goals confusing because it says uniformity without saying what is the base type. Of course there are intermediate options, like having two defs, but I fear this will lead to pain. I'm also in favor of having a local notation for this, as in my Amsterdam talk (I use mathcal U for the def with explicit α).

[Johannes Hölzl]

I'm fine with this change i think replacing ([^@])uniformity with \1(uniformity _) should solve most errors.

[Patrick Massot]

https://github.com/leanprover-community/mathlib/pull/814

[Johan Commelin]

Lol, the @uniformity in the commit message confuses GitHub, who thinks we are trying to mention a user. If you've always been looking for a nice GitHub handle... here's your chance: @uniformity is currently free.

[Johan Commelin]

And congrats to @Patrick Massot for getting this in mathlib. Thanks for doing all this tedious work! :tada: :octopus: