English
Let e : X → Y and e' : Y → Z be homeomorphisms and f'' : OpenPartialHomeomorph Z Z'. Then the two ways of composing them satisfy associativity: (e.trans e').transOpenPartialHomeomorph f'' = e.transOpenPartialHomeomorph (e'.transOpenPartialHomeomorph f'').
Русский
Пусть e : X → Y и e' : Y → Z — гомеоморфизмы, а f'' : OpenPartialHomeomorph Z Z'. Тогда два способа их композиции дают одинаковый результат: (e.trans e').transOpenPartialHomeomorph f'' = e.transOpenPartialHomeomorph (e'.transOpenPartialHomeomorph f'').
LaTeX
$$$ (e \\text{ trans } e') \\text{ transOpenPartialHomeomorph } f'' = e \\text{ transOpenPartialHomeomorph } (e' \\text{ transOpenPartialHomeomorph } f'') $$$
Lean4
@[simp, mfld_simps]
theorem trans_transOpenPartialHomeomorph (e : X ≃ₜ Y) (e' : Y ≃ₜ Z) (f'' : OpenPartialHomeomorph Z Z') :
(e.trans e').transOpenPartialHomeomorph f'' = e.transOpenPartialHomeomorph (e'.transOpenPartialHomeomorph f'') := by
simp only [transOpenPartialHomeomorph_eq_trans, OpenPartialHomeomorph.trans_assoc, trans_toOpenPartialHomeomorph]
