English
Let e: X → Y and f: Y → Z be open partial homeomorphisms, and e': X' → Y' and f': Y' → Z' another pair. Then the product operation on pairs is compatible with composition, i.e. the composed product equals the product of the compositions: (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f').
Русский
Пусть e: X → Y и f: Y → Z — частичные открытые гомеоморфизмы, а также e': X' → Y' и f': Y' → Z' — другая пара. Тогда произведение пар и композиции согласованы: (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f').
LaTeX
$$$ (e \;prod\; e').trans (f \;prod\; f') = (e \trans f) \;prod\ (e' \trans f') $$$
Lean4
@[simp, mfld_simps]
theorem prod_trans (e : OpenPartialHomeomorph X Y) (f : OpenPartialHomeomorph Y Z) (e' : OpenPartialHomeomorph X' Y')
(f' : OpenPartialHomeomorph Y' Z') : (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f') :=
toPartialEquiv_injective <| e.1.prod_trans ..
