transOpenPartialHomeomorph_trans — Mathlib

English

A Homeomorph and an OpenPartialHomeomorph compose to give an OpenPartialHomeomorph in a predictable manner; the equality mirrors the standard trans.

Русский

Гомеоморфизм и OpenPartialHomeomorph образуют OpenPartialHomeomorph по предсказуемому правилу; равенство аналогично стандартному trans.

LaTeX

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

Lean4

@[simp, mfld_simps]
theorem transOpenPartialHomeomorph_trans (e : X ≃ₜ Y) (f : OpenPartialHomeomorph Y Z)
    (f' : OpenPartialHomeomorph Z Z') :
    (e.transOpenPartialHomeomorph f).trans f' = e.transOpenPartialHomeomorph (f.trans f') := by
  simp only [transOpenPartialHomeomorph_eq_trans, OpenPartialHomeomorph.trans_assoc]

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