## Stream: maths

### Topic: uniform lemma

#### 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')


#### 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


#### 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

#### 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

#### Mario Carneiro (Jul 15 2018 at 02:14):

Maybe apply_eq_of_separated for the second?

#### 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.

#### 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.

#### 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.

#### 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.

#### 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 :-)

#### Kenny Lau (Jul 15 2018 at 12:59):

I think every mathematician should read Bourbaki in a bar

#### 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.

#### 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