Zulip Chat Archive

Stream: new members

Topic: translation on reals


view this post on Zulip Damiano Testa (Dec 23 2020 at 15:04):

Dear All,

I am struggling to find a proof of the lemma below: I am convinced that it should be in mathlib, I have found continuous_add, but I know so little od the topology side of mathlib, that I am unable to get it to work. Can anyone give me a pointer, please?

Thanks!

import analysis.convex.topology

open real

lemma translate_open (α : ) (U : set ) (oU : is_open U) :
  is_open ((λ (y : ), y - α) '' U) :=
begin
  sorry,
end

view this post on Zulip Kenny Lau (Dec 23 2020 at 15:14):

#xy

view this post on Zulip Damiano Testa (Dec 23 2020 at 15:22):

I have a set A of reals and a real x ∈ A. I want to show that A \ {x} ≠ ∅ by showing that A contains a neighbourhood of x. The neighbourhood in question is the translate of an intersection of sets that I already know are open and nonempty, hence the question!

view this post on Zulip Johan Commelin (Dec 23 2020 at 15:23):

@Damiano Testa there is continuous_add_left

view this post on Zulip Johan Commelin (Dec 23 2020 at 15:23):

the first thing I would do is change your goal to preimage under addition, instead of images under subtraction.

view this post on Zulip Damiano Testa (Dec 23 2020 at 15:24):

Hmm, maybe I should import more? I get

unknown identifier 'has_continuous_add_left'

view this post on Zulip Damiano Testa (Dec 23 2020 at 15:24):

Let me try with replacing preimages!

view this post on Zulip Johan Commelin (Dec 23 2020 at 15:24):

without the has_

view this post on Zulip Kenny Lau (Dec 23 2020 at 15:25):

or better, use the preimage under addition instead of the image under subtraction as your neighbourhood

view this post on Zulip Damiano Testa (Dec 23 2020 at 15:27):

I will try to make this work, thanks!

view this post on Zulip Damiano Testa (Dec 23 2020 at 15:29):

This works!

lemma translate_open (α : ) (U : set ) (oU : is_open U) :
  is_open ((λ (y : ), y + α) ⁻¹' U) :=
continuous_add_right α U oU

Now I will adjust the rest to what I have!

view this post on Zulip Damiano Testa (Dec 23 2020 at 15:36):

There is even preimage_add_const_Ioo! Found by simp!

view this post on Zulip Adam Topaz (Dec 23 2020 at 15:52):

Is there no homeomorph_add_left in mathlib?

view this post on Zulip Heather Macbeth (Dec 23 2020 at 15:54):

docs#homeomorph.add_left

view this post on Zulip Damiano Testa (Dec 23 2020 at 16:21):

Ah, thanks for the pointer to homeomorph.add_left! I am doing some very simple-minded argument, so I may not be needing it, but I am relieved to see that it is in mathlib!


Last updated: May 15 2021 at 02:11 UTC