Zulip Chat Archive

Stream: Is there code for X?

Topic: a lemma about --inducing-- open_embedding?


Scott Morrison (Jul 27 2020 at 13:59):

import topology.local_homeomorph

lemma open_embedding.continuous_at_iff
  {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} :
  continuous_at (g  f) x  continuous_at g (f x) :=
begin
  haveI : nonempty X := x,
  convert ((hf.to_local_homeomorph.continuous_at_iff_continuous_at_comp_right) _).symm,
  { apply (local_homeomorph.left_inv _ _).symm,
    simp, },
  { simp, },
end

Last updated: Dec 20 2023 at 11:08 UTC