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

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

bingo

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

Hmn, I could PR the continuity tactic now that tidy is in mathlib