∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e e' : OpenPartialHomeomorph X Y) (s : Set X),
  e.source ∩ frontier s = e'.source ∩ frontier s → IsOpen (s.ite e.source e'.source)