Zulip Chat Archive

Stream: maths

Topic: uniformity


view this post on Zulip Patrick Massot (Mar 08 2019 at 09:24):

@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 α).

view this post on Zulip Johannes Hölzl (Mar 08 2019 at 14:42):

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

view this post on Zulip Patrick Massot (Mar 12 2019 at 11:23):

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

view this post on Zulip Johan Commelin (Mar 12 2019 at 14:40):

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.

view this post on Zulip Johan Commelin (Mar 12 2019 at 14:40):

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


Last updated: May 10 2021 at 07:15 UTC