English
Let e : X → Y and e' : Y → Z be OpenPartialHomeomorphs and f'' : Homeomorph Z Z'. Then the associative law holds: (e.trans e').transHomeomorph f'' = e.transHomeomorph (e'.transHomeomorph f'').
Русский
Пусть e : X → Y и e' : Y → Z — OpenPartialHomeomorph, а f'' : Homeomorph Z Z'. Тогда выполняется ассоциативное свойство: (e.trans e').transHomeomorph f'' = e.transHomeomorph (e'.transHomeomorph f'').
LaTeX
$$$ (e.trans e').transHomeomorph f'' = e.transHomeomorph (e'.transHomeomorph f'') $$$
Lean4
@[simp, mfld_simps]
theorem transHomeomorph_transHomeomorph (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z) (f'' : Z ≃ₜ Z') :
(e.transHomeomorph f').transHomeomorph f'' = e.transHomeomorph (f'.trans f'') := by
simp only [transHomeomorph_eq_trans, trans_assoc, Homeomorph.trans_toOpenPartialHomeomorph]