trans' — Mathlib

English

Composition of open partial homeomorphisms respects equivalence: if e ≈ e' and f ≈ f', then e.trans f ≈ e'.trans f'.

Русский

Состав открытых частичных гомеоморфизмов сохраняет эквивалентность: если e ≈ e' и f ≈ f', то e.trans f ≈ e'.trans f'.

LaTeX

$$$ (e \approx e') \land (f \approx f') \Rightarrow (e.trans f) \approx (e'.trans f') $$$

Lean4

/-- Composition of open partial homeomorphisms respects equivalence. -/
theorem trans' {e e' : OpenPartialHomeomorph X Y} {f f' : OpenPartialHomeomorph Y Z} (he : e ≈ e') (hf : f ≈ f') :
    e.trans f ≈ e'.trans f' :=
  PartialEquiv.EqOnSource.trans' he hf

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