English
If an OpenPartialHomeomorph arises from a Homeomorph with univ source, then it is an open embedding.
Русский
Если OpenPartialHomeomorph порождается Homeomorph с источником univ, то это открытое вложение.
LaTeX
$$$to_isOpenEmbedding : IsOpenEmbedding (e.source.restrict e.toFun')$$$
Lean4
/-- Precompose an open partial homeomorphism with a homeomorphism.
We modify the source and target to have better definitional behavior. -/
@[simps! -fullyApplied]
def transOpenPartialHomeomorph (e : X ≃ₜ Y) (f' : OpenPartialHomeomorph Y Z) : OpenPartialHomeomorph X Z
where
toPartialEquiv := e.toEquiv.transPartialEquiv f'.toPartialEquiv
open_source := f'.open_source.preimage e.continuous
open_target := f'.open_target
continuousOn_toFun := f'.continuousOn.comp e.continuous.continuousOn fun _ => id
continuousOn_invFun := e.symm.continuous.comp_continuousOn f'.symm.continuousOn
