Zulip Chat Archive

Stream: maths

Topic: uniform lemma


view this post on Zulip Patrick Massot (Jul 14 2018 at 21:47):

Is the following lemma already hidden somewhere in mathlib? Or is it too trivial to be stated? What would be his canonical name?

import analysis.topology.uniform_space

local attribute [instance] separation_setoid

variables {α : Type*} [uniform_space α]
variables {β : Type*} [uniform_space β]

lemma separation_rel_of_uniform_continuous {f : α  β} (H : uniform_continuous f) {x y : α}
(h : x  y) : f x  f y :=
assume _ h', h _ (H h')

view this post on Zulip Patrick Massot (Jul 14 2018 at 21:56):

Same question for the obvious corollary

lemma image_eq_of_uniform_continuous_of_separated [separated β] {f : α  β} (H : uniform_continuous f) {x y : α}
(h : x  y) : f x = f y :=
separated_def.1 (by apply_instance) _ _ $ separation_rel_of_uniform_continuous H h

view this post on Zulip Patrick Massot (Jul 14 2018 at 21:57):

@Mario Carneiro I know this is Johannes domain, but I'd be interested in your opinion about naming here

view this post on Zulip Mario Carneiro (Jul 15 2018 at 02:13):

That's a tough one. I don't like the use of the word image in the second one, that connotes '' but it doesn't appear in the statement

view this post on Zulip Mario Carneiro (Jul 15 2018 at 02:14):

Maybe apply_eq_of_separated for the second?

view this post on Zulip Patrick Massot (Jul 15 2018 at 10:02):

Ok. It leaves out most of the statement but I don't see how to avoid that when there are so many hypotheses.

view this post on Zulip Johannes Hölzl (Jul 15 2018 at 12:15):

I think separated_of_uniform_continuous and eq_of_separated_of_uniform_continuous would be also okay.

view this post on Zulip Patrick Massot (Jul 15 2018 at 12:32):

Thanks. I now use these names since you will have to review a PR containing all this at some point.

view this post on Zulip Patrick Massot (Jul 15 2018 at 12:57):

Now, for something really weird, I'll try to go read Bourbaki GT in a bar, hoping this will secure me some place to watch the game. It may be too late already.

view this post on Zulip Patrick Massot (Jul 15 2018 at 12:59):

Maybe I should point out that my wife and kids are in vacations, so I'm alone at home. Otherwise I wouldn't do that :-)

view this post on Zulip Kenny Lau (Jul 15 2018 at 12:59):

I think every mathematician should read Bourbaki in a bar

view this post on Zulip Patrick Massot (Jul 15 2018 at 17:54):

It worked out pretty nicely. Now I know what are the supporting lemmas that I need to prove about completions.

view this post on Zulip Patrick Massot (Jul 15 2018 at 17:55):

Kenny, reading and doing math in bar is very standard, what was slightly weird was the atmosphere around me. But I was able to mostly work until about 15 minutes before the beginning.


Last updated: May 06 2021 at 19:30 UTC