English
The subtype-restricted open partial homeomorphism e.subtypeRestr hs is the composition of the openPartialHomeomorphSubtypeCoe hs with e.
Русский
Открыто-частичный гомеоморфизм, ограниченный подтипом e.subtypeRestr hs, равен композиции s.openPartialHomeomorphSubtypeCoe hs с e.
LaTeX
$$$ e.subtypeRestr hs = (s.openPartialHomeomorphSubtypeCoe hs).trans e $$$
Lean4
/-- Postcompose an open partial homeomorphism with a homeomorphism.
We modify the source and target to have better definitional behavior. -/
@[simps! -fullyApplied]
def transHomeomorph (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z) : OpenPartialHomeomorph X Z
where
toPartialEquiv := e.toPartialEquiv.transEquiv f'.toEquiv
open_source := e.open_source
open_target := e.open_target.preimage f'.symm.continuous
continuousOn_toFun := f'.continuous.comp_continuousOn e.continuousOn
continuousOn_invFun := e.symm.continuousOn.comp f'.symm.continuous.continuousOn fun _ => id
