English
If source equals univ, then the corresponding OpenPartialHomeomorph yields an open embedding of X into Y.
Русский
Если источник равен всему X, то соответствующий OpenPartialHomeomorph задаёт открытое вложение X в Y.
LaTeX
$$$to_isOpenEmbedding : e.source = univ \Rightarrow IsOpenEmbedding e.toFun'$$$
Lean4
/-- If an open partial homeomorphism has source and target equal to univ, then it induces a
homeomorphism between the whole spaces, expressed in this definition. -/
@[simps (attr := mfld_simps) -fullyApplied apply symm_apply]
-- TODO: add a `PartialEquiv` version
def toHomeomorphOfSourceEqUnivTargetEqUniv (h : e.source = (univ : Set X)) (h' : e.target = univ) : X ≃ₜ Y
where
toFun := e
invFun := e.symm
left_inv
x :=
e.left_inv <| by
rw [h]
exact mem_univ _
right_inv
x :=
e.right_inv <| by
rw [h']
exact mem_univ _
continuous_toFun := by simpa only [continuousOn_univ, h] using e.continuousOn
continuous_invFun := by simpa only [continuousOn_univ, h'] using e.continuousOn_symm
