English
The inverse of an open partial homeomorphism is again an open partial homeomorphism with swapped source/target and reversed continuity directions.
Русский
Обратное открытой частичной гомеоморфизмы есть снова открытая частичная гомеоморфизма с поменянными источником/целевым пространства и обращенными условиями непрерывности.
LaTeX
$$$OpenPartialHomeomorph.symm : OpenPartialHomeomorph Y X$ is defined with swapped sources/targets and swapped continuity flags.$$
Lean4
/-- The inverse of an open partial homeomorphism -/
@[symm]
protected def symm : OpenPartialHomeomorph Y X
where
toPartialEquiv := e.toPartialEquiv.symm
open_source := e.open_target
open_target := e.open_source
continuousOn_toFun := e.continuousOn_invFun
continuousOn_invFun := e.continuousOn_toFun
