{X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (e : X ≃ₜ Y) → (s : Set X) → IsOpen s → (t : Set Y) → ⇑e '' s = t → OpenPartialHomeomorph X Y