English
Two open partial homeomorphisms can be composed when the target of the first matches the source of the second, yielding another open partial homeomorphism.
Русский
Две открытые частичные гомеоморфизмы можно композициировать, если целевая область первого совпадает с областью определения второго, и получится новый открытый частичный гомеоморфизм.
LaTeX
$$$\\text{protected def } \\mathrm{trans'}(h): \\mathrm{OpenPartialHomeomorph}~X~Z \\,,$$$
Lean4
/-- Composition of two open partial homeomorphisms when the target of the first and the source of
the second coincide. -/
@[simps! apply symm_apply toPartialEquiv, simps! -isSimp source target]
protected def trans' (h : e.target = e'.source) : OpenPartialHomeomorph X Z
where
toPartialEquiv := PartialEquiv.trans' e.toPartialEquiv e'.toPartialEquiv h
open_source := e.open_source
open_target := e'.open_target
continuousOn_toFun := e'.continuousOn.comp e.continuousOn <| h ▸ e.mapsTo
continuousOn_invFun := e.continuousOn_symm.comp e'.continuousOn_symm <| h.symm ▸ e'.symm_mapsTo
