Zulip Chat Archive

Stream: new members

Topic: translation on reals

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

Kenny Lau (Dec 23 2020 at 15:14):

#xy

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!

Johan Commelin (Dec 23 2020 at 15:23):

@Damiano Testa there is continuous_add_left

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.

Damiano Testa (Dec 23 2020 at 15:24):

Hmm, maybe I should import more? I get

unknown identifier 'has_continuous_add_left'

Damiano Testa (Dec 23 2020 at 15:24):

Let me try with replacing preimages!

Johan Commelin (Dec 23 2020 at 15:24):

without the has_

Kenny Lau (Dec 23 2020 at 15:25):

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

Damiano Testa (Dec 23 2020 at 15:27):

I will try to make this work, thanks!

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!

Damiano Testa (Dec 23 2020 at 15:36):

There is even preimage_add_const_Ioo! Found by simp!

Adam Topaz (Dec 23 2020 at 15:52):

Is there no homeomorph_add_left in mathlib?

Heather Macbeth (Dec 23 2020 at 15:54):

docs#homeomorph.add_left

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: Dec 20 2023 at 11:08 UTC