∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (h : X ≃ₜ Y) (f : Z → X) (z : Z), ContinuousAt (⇑h ∘ f) z ↔ ContinuousAt f z