a lemma about inducing?

Stream: Is there code for X?

[Scott Morrison]

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]

I guess it must be basically inducing.tendsto_nhds_iff

[Johan Commelin]

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

[Johan Commelin]

Maybe the lemma is not even true?

[Johan Commelin]

We might need open_embedding f?

[Reid Barton]

Oh whoops, you're right

[Reid Barton]

X could be empty

[Reid Barton]

Scott probably confused by >> order :upside_down:

[Johan Commelin]

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

[Reid Barton]

okay, not empty but a point

[Scott Morrison]

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

[Scott Morrison]

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]

/me was over-optimistic...

[Reid Barton]

is continuous_at_iff_continuous_at_comp_right useful?

[Reid Barton]

/me has never used continuous_at

[Scott Morrison]

That did it, thanks!