English
Composition of open partial homeomorphisms is associative; composing e with e' and then with e'' equals composing e with the composition of e' and e''.
Русский
Сложение открытых частичных гомеоморфизмов является ассоциативным: (e trans e') trans e'' = e trans (e' trans e'').
LaTeX
$$$ (e.trans e').trans e'' = e.trans (e'.trans e'') $$$
Lean4
/-- Composing two open partial homeomorphisms, by restricting to the maximal domain where their
composition is well defined.
Within the `Manifold` namespace, there is the notation `e ≫ₕ f` for this. -/
@[trans]
protected def trans : OpenPartialHomeomorph X Z :=
OpenPartialHomeomorph.trans' (e.symm.restrOpen e'.source e'.open_source).symm (e'.restrOpen e.target e.open_target)
(by simp [inter_comm])
