English
Replacing the underlying partial equivalence of an open partial homeomorphism by another one with the same action yields the same object.
Русский
Замена базовой частичной эквивалентности у открытого частичного гомеоморфа на другую с тем же действием не изменяет сам объект.
LaTeX
$$$\forall e: OpenPartialHomeomorph\,X\,Y,\forall e': PartialEquiv\,X\,Y,\forall h: e.toPartialEquiv = e',\ e.replaceEquiv\,e'\,h = e.$$$
Lean4
/-- Replace `toPartialEquiv` field to provide better definitional equalities. -/
def replaceEquiv (e : OpenPartialHomeomorph X Y) (e' : PartialEquiv X Y) (h : e.toPartialEquiv = e') :
OpenPartialHomeomorph X Y where
toPartialEquiv := e'
open_source := h ▸ e.open_source
open_target := h ▸ e.open_target
continuousOn_toFun := h ▸ e.continuousOn_toFun
continuousOn_invFun := h ▸ e.continuousOn_invFun
