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 R\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):

Related: https://github.com/leanprover-community/mathlib/blob/completions/analysis/topology/topological_structures.lean#L289

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

Reid: yes, please!


Last updated: Dec 20 2023 at 11:08 UTC