∀ {X : Type u_2} {Y : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.IsImage s t → IsOpen (e.source ∩ s) → IsOpen (e.target ∩ t)