uniform lemma

Stream: maths

[Patrick Massot]

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]

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]

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

[Mario Carneiro]

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]

Maybe apply_eq_of_separated for the second?

[Patrick Massot]

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]

I think separated_of_uniform_continuous and eq_of_separated_of_uniform_continuous would be also okay.

[Patrick Massot]

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

[Patrick Massot]

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]

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]

I think every mathematician should read Bourbaki in a bar

[Patrick Massot]

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

[Patrick Massot]

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.