Scaling of open set is open

Stream: Is there code for X?

[Bhavik Mehta]

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

[Kevin Buzzard]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

Ah, got it

[Bhavik Mehta]

I needed is_open_map_smul' not is_open_map_smul

[Bhavik Mehta]

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

[Yakov Pechersky]

exact hx.ne'

[Bhavik Mehta]

Oh neat trick, thanks

[Kevin Buzzard]

He's the dot notation master :-)

[Kevin Buzzard]

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).

[Yakov Pechersky]

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