transOpenPartialHomeomorph_eq_trans

English

Equality of trans between Homeomorphs and OpenPartialHomeomorphs aligns with trans of images under the toPartialEquiv map.

Русский

Равенство trans между гомеоморфизмами согласуется с trans образов под toPartialEquiv.

LaTeX

$$$(e : X \simeq Y).transOpenPartialHomeomorph f' = e.toOpenPartialHomeomorph.trans f'$$$

Lean4

theorem transOpenPartialHomeomorph_eq_trans (e : X ≃ₜ Y) (f' : OpenPartialHomeomorph Y Z) :
    e.transOpenPartialHomeomorph f' = e.toOpenPartialHomeomorph.trans f' :=
  OpenPartialHomeomorph.toPartialEquiv_injective <| Equiv.transPartialEquiv_eq_trans _ _

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