is_open {x | x + u \in U}

Stream: general

[Johan Commelin]

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]

continuous_add or something

[Kevin Buzzard]

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]

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

[Johan Commelin]

Hmmm, I probably over-generalised.

[Johan Commelin]

Let's assume it's a group.

[Kevin Buzzard]

then what Kenny said

[Johannes Hölzl]

Huh, the title looks like a preimage

[Johan Commelin]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

which is continuous for any topological space

[Kenny Lau]

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]

bingo

[Reid Barton]

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

[Patrick Massot]

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

[Patrick Massot]

Reid: yes, please!