∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : X} (p : X → Prop),
  x ∈ e.source → ((∀ᶠ (y : Y) in nhds (↑e x), p (↑e.symm y)) ↔ ∀ᶠ (x : X) in nhds x, p x)