Zulip Chat Archive

Stream: Is there code for X?

Topic: a lemma about inducing?


view this post on Zulip 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

view this post on Zulip Reid Barton (Jul 27 2020 at 13:33):

I guess it must be basically inducing.tendsto_nhds_iff

view this post on Zulip Johan Commelin (Jul 27 2020 at 13:38):

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

view this post on Zulip Johan Commelin (Jul 27 2020 at 13:38):

Maybe the lemma is not even true?

view this post on Zulip Johan Commelin (Jul 27 2020 at 13:38):

We might need open_embedding f?

view this post on Zulip Reid Barton (Jul 27 2020 at 13:39):

Oh whoops, you're right

view this post on Zulip Reid Barton (Jul 27 2020 at 13:39):

X could be empty

view this post on Zulip Reid Barton (Jul 27 2020 at 13:39):

Scott probably confused by >> order :upside_down:

view this post on Zulip Johan Commelin (Jul 27 2020 at 13:40):

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

view this post on Zulip Reid Barton (Jul 27 2020 at 13:40):

okay, not empty but a point

view this post on Zulip Scott Morrison (Jul 27 2020 at 13:40):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 27 2020 at 13:40):

/me was over-optimistic...

view this post on Zulip Reid Barton (Jul 27 2020 at 13:44):

is continuous_at_iff_continuous_at_comp_right useful?

view this post on Zulip Reid Barton (Jul 27 2020 at 13:44):

/me has never used continuous_at

view this post on Zulip Scott Morrison (Jul 27 2020 at 13:51):

That did it, thanks!


Last updated: May 07 2021 at 22:14 UTC