{X : Type u_7} →
  {Y : Type u_8} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (toPartialEquiv : PartialEquiv X Y) →
          IsOpen toPartialEquiv.source →
            IsOpen toPartialEquiv.target →
              ContinuousOn (↑toPartialEquiv) toPartialEquiv.source →
                ContinuousOn toPartialEquiv.invFun toPartialEquiv.target → OpenPartialHomeomorph X Y