## Stream: Is there code for X?

### Topic: a lemma about inducing?

#### Scott Morrison (Jul 27 2020 at 13:28):

import topology.continuous_on

lemma inducing.foo {X Y Z : Type*} [topological_space X] [topological_space Y] [topological_space Z]
{f : X → Y} {g : Y → Z} (hf : inducing f) {x : X} (h : continuous_at (g ∘ f) x) :
continuous_at g (f x) :=
sorry


#### Reid Barton (Jul 27 2020 at 13:33):

I guess it must be basically inducing.tendsto_nhds_iff

#### Johan Commelin (Jul 27 2020 at 13:38):

That works on the wrong side of the composition...

#### Johan Commelin (Jul 27 2020 at 13:38):

Maybe the lemma is not even true?

#### Johan Commelin (Jul 27 2020 at 13:38):

We might need open_embedding f?

#### Reid Barton (Jul 27 2020 at 13:39):

Oh whoops, you're right

#### Reid Barton (Jul 27 2020 at 13:39):

X could be empty

#### Reid Barton (Jul 27 2020 at 13:39):

Scott probably confused by >> order :upside_down:

#### Johan Commelin (Jul 27 2020 at 13:40):

There is an x : X in the statement...

#### Reid Barton (Jul 27 2020 at 13:40):

okay, not empty but a point

#### Scott Morrison (Jul 27 2020 at 13:40):

no, we were just be over-optimistic :-) in our setting we already know open_embedding f.

#### Scott Morrison (Jul 27 2020 at 13:40):

So here's the new target:

lemma open_embedding.foo {X Y Z : Type*} [topological_space X] [topological_space Y] [topological_space Z]
{f : X → Y} {g : Y → Z} (hf : open_embedding f) {x : X} (h : continuous_at (g ∘ f) x) :
continuous_at g (f x) :=
begin

end


#### Johan Commelin (Jul 27 2020 at 13:40):

/me was over-optimistic...

#### Reid Barton (Jul 27 2020 at 13:44):

is continuous_at_iff_continuous_at_comp_right useful?

#### Reid Barton (Jul 27 2020 at 13:44):

/me has never used continuous_at

#### Scott Morrison (Jul 27 2020 at 13:51):

That did it, thanks!

Last updated: May 07 2021 at 22:14 UTC