toHomeomorph_trans — Mathlib

English

The homeomorph of a composition equals the composition of the homeomorphs.

Русский

Гомеоморфизм композиции равен композиции гомеоморфизмов.

LaTeX

$$$ (e.trans f).toHomeomorph (\\lambda s. (he s).trans (hf s)) = (e.toHomeomorph he).trans (f.toHomeomorph hf) $$$

Lean4

theorem toHomeomorph_trans (e : X ≃ Y) (f : Y ≃ Z) (he hf) :
    (e.trans f).toHomeomorph (fun _s ↦ (he _).trans (hf _)) = (e.toHomeomorph he).trans (f.toHomeomorph hf) :=
  rfl

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