transHomeomorph_transHomeomorph — Mathlib

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]

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