transHomeomorph_eq_trans — Mathlib

English

The symmetric-transitive composition of subtypeRestr maps corresponds to restricting the symmetric composition of the original maps to the intersection domain, up to a set-theoretic equivalence.

Русский

Симметрично-пересечение композиции ограничений по подтипу соответствует симметричной композиции исходных отображений, ограниченной областью пересечения, в эквивалентности множестового типа.

LaTeX

$$$ (f.subtypeRestr hs)^{-1} \circ (f'.subtypeRestr hs) \approx (f^{-1}.trans f').restr (f.target \cap f^{-1}'' s) $$$

Lean4

theorem transHomeomorph_eq_trans (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z) :
    e.transHomeomorph f' = e.trans f'.toOpenPartialHomeomorph :=
  toPartialEquiv_injective <| PartialEquiv.transEquiv_eq_trans _ _

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