Zulip Chat Archive

Stream: Is there code for X?

Topic: Scaling of open set is open


view this post on Zulip Bhavik Mehta (Apr 15 2021 at 17:22):

lemma is_open_smul {α : Type*} [normed_group α] [normed_space  α] (X : set α) (hX : is_open X)
  (x : ) (hx : 0 < x) :
  is_open (x  X) :=
begin
end

Probably the assumptions can be weakened - I expect this doesn't need a norm but I'm not sure which class exactly is correct, I'm also struggling to find helpful lemmas in mathlib for this

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 17:23):

I guess this will be true for any topological vector space, because mulitplication by x^{-1} is continuous

view this post on Zulip Bhavik Mehta (Apr 15 2021 at 17:24):

My Lean can't find topological_vector_space though - that was my first guess too

view this post on Zulip Bhavik Mehta (Apr 15 2021 at 17:25):

Ah, got it

view this post on Zulip Bhavik Mehta (Apr 15 2021 at 17:25):

I needed is_open_map_smul' not is_open_map_smul

view this post on Zulip Bhavik Mehta (Apr 15 2021 at 17:25):

lemma is_open_smul {α : Type*} [normed_group α] [normed_space  α] (X : set α) (hX : is_open X)
  (x : ) (hx : 0 < x) :
  is_open (x  X) :=
begin
  suffices : is_open_map (λ (y:α), x  y),
  { apply this,
    apply hX },
  apply is_open_map_smul',
  apply ne_of_gt hx,
end

view this post on Zulip Yakov Pechersky (Apr 15 2021 at 17:27):

exact hx.ne'

view this post on Zulip Bhavik Mehta (Apr 15 2021 at 17:29):

Oh neat trick, thanks

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 17:39):

He's the dot notation master :-)

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 17:40):

It's little tricks like this which really open your eyes to how this dot notation can be used. Apparently this is Leo's insight (this is my understanding from Jeremy at least).

view this post on Zulip Yakov Pechersky (Apr 15 2021 at 17:42):

I still think Yury is the dot notation expert. I just read his refactoring PRs


Last updated: May 07 2021 at 22:14 UTC