Zulip Chat Archive

Stream: general

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


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Sep 10 2018 at 18:28):

continuous_add or something

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Sep 10 2018 at 18:30):

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

view this post on Zulip Johan Commelin (Sep 10 2018 at 18:31):

Hmmm, I probably over-generalised.

view this post on Zulip Johan Commelin (Sep 10 2018 at 18:31):

Let's assume it's a group.

view this post on Zulip Kevin Buzzard (Sep 10 2018 at 18:31):

then what Kenny said

view this post on Zulip Johannes Hölzl (Sep 10 2018 at 18:31):

Huh, the title looks like a preimage

view this post on Zulip Johan Commelin (Sep 10 2018 at 18:31):

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

view this post on Zulip Kevin Buzzard (Sep 10 2018 at 18:32):

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

view this post on Zulip Johan Commelin (Sep 10 2018 at 18:32):

Ok, somehow continuous_add didn't work straightaway. I'll try harder.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 10 2018 at 18:33):

which is continuous for any topological space

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 10 2018 at 18:44):

bingo

view this post on Zulip Reid Barton (Sep 10 2018 at 18:46):

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

view this post on Zulip Patrick Massot (Sep 10 2018 at 18:59):

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

view this post on Zulip Patrick Massot (Sep 10 2018 at 18:59):

Reid: yes, please!


Last updated: May 15 2021 at 23:13 UTC