trans_transHomeomorph — Mathlib

English

For any OpenPartialHomeomorphs e and e' and a Homeomorph f'': (e.trans e').transHomeomorph f'' = e.trans (e'.transHomeomorph f'').

Русский

Для любых OpenPartialHomeomorphs e и e' и гомеоморфизма f'': (e.trans e').transHomeomorph f'' = e.trans (e'.transHomeomorph f'').

LaTeX

$$$ (e.trans e').transHomeomorph f'' = e.trans (e'.transHomeomorph f'') $$$

Lean4

@[simp, mfld_simps]
theorem trans_transHomeomorph (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) (f'' : Z ≃ₜ Z') :
    (e.trans e').transHomeomorph f'' = e.trans (e'.transHomeomorph f'') := by
  simp only [transHomeomorph_eq_trans, trans_assoc]

Похожие утверждения