# Zulip Chat Archive

## Stream: general

### Topic: is_open {x | x + u \in U}

#### Johan Commelin (Sep 10 2018 at 18:19):

Given a topological additive monoid, I expected theorems that say that you can translate opens along addition by a given element. But I could not find those... is this in mathlib, or do I need to roll my own?

#### Kenny Lau (Sep 10 2018 at 18:28):

continuous_add or something

#### Kevin Buzzard (Sep 10 2018 at 18:30):

Are you sure Kenny? That seems to prove only that the pre-image of an open under the map lam x, x+c (c constant) is open. But you can't cancel in a monoid and Johan seems to want to show that the image, not the pre-image, of an open is open. @Johan Commelin are you sure that what you want to prove is true? What exactly do you want to prove?

#### Kevin Buzzard (Sep 10 2018 at 18:30):

and what exactly are you thinking about topological monoids for??

#### Johan Commelin (Sep 10 2018 at 18:31):

Hmmm, I probably over-generalised.

#### Johan Commelin (Sep 10 2018 at 18:31):

Let's assume it's a group.

#### Kevin Buzzard (Sep 10 2018 at 18:31):

then what Kenny said

#### Johannes Hölzl (Sep 10 2018 at 18:31):

Huh, the title looks like a preimage

#### Johan Commelin (Sep 10 2018 at 18:31):

That's good enough for applications, since I'm a mathematician.

#### Kevin Buzzard (Sep 10 2018 at 18:32):

oh yes, Kenny's comment answers the question in the title but not in the body.

#### Johan Commelin (Sep 10 2018 at 18:32):

Ok, somehow `continuous_add`

didn't work straightaway. I'll try harder.

#### Kevin Buzzard (Sep 10 2018 at 18:32):

I'm assuming continuous_add is continuity of addition, so now you need to compose with the map from G to G x G sending g to g,c

#### Kevin Buzzard (Sep 10 2018 at 18:33):

which is continuous for any topological space

#### Kenny Lau (Sep 10 2018 at 18:43):

Given a topological additive monoid, I expected theorems that say that you can translate opens along addition by a given element. But I could not find those... is this in mathlib, or do I need to roll my own?

I think this is not true. Consider the topological multiplicative monoid $\Bbb R$ and translation by 0

#### Kevin Buzzard (Sep 10 2018 at 18:44):

bingo

#### Reid Barton (Sep 10 2018 at 18:46):

Hmn, I could PR the `continuity`

tactic now that tidy is in mathlib

#### Patrick Massot (Sep 10 2018 at 18:59):

#### Patrick Massot (Sep 10 2018 at 18:59):

Reid: yes, please!

Last updated: May 15 2021 at 23:13 UTC