## Stream: Is there code for X?

### Topic: Scaling of open set is open

#### 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

#### 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

#### Bhavik Mehta (Apr 15 2021 at 17:24):

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

Ah, got it

#### Bhavik Mehta (Apr 15 2021 at 17:25):

I needed is_open_map_smul' not is_open_map_smul

#### 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


#### Yakov Pechersky (Apr 15 2021 at 17:27):

exact hx.ne'

#### Bhavik Mehta (Apr 15 2021 at 17:29):

Oh neat trick, thanks

#### Kevin Buzzard (Apr 15 2021 at 17:39):

He's the dot notation master :-)

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

#### 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