restr_trans — Mathlib

English

Let e: OpenPartialHomeomorph X Y and e': OpenPartialHomeomorph Y Z be open partial homeomorphisms. For any set s ⊆ X, the transitive composition respects restriction: (e.restr s).trans e' = (e.trans e').restr s.

Русский

Пусть e: OpenPartialHomeomorph X Y и e': OpenPartialHomeomorph Y Z — открытые частичные гомеоморфизмы. Для множества s ⊆ X выполняется, что (e.restr s).trans e' = (e.trans e').restr s.

LaTeX

$$$ (e.restr s).trans e' = (e.trans e').restr s $$$

Lean4

theorem restr_trans (s : Set X) : (e.restr s).trans e' = (e.trans e').restr s :=
  toPartialEquiv_injective <| PartialEquiv.restr_trans e.toPartialEquiv e'.toPartialEquiv (interior s)

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