English
If φ: X ≃ₜ Z and ψ: Y ≃ₜ T are homeomorphisms, then the induced map C(X, Y) ≃ₜ C(Z, T) given by f ↦ ψ ∘ f ∘ φ⁻¹ is a homeomorphism.
Русский
Если существуют домашоморфизмы φ: X ≃ₜ Z и ψ: Y ≃ₜ T, то отображение на пространствах функций f ↦ ψ ∘ f ∘ φ⁻¹ даёт гомеоморфизм C(X,Y) ≃ₜ C(Z,T).
LaTeX
$$$\\text{Homeomorph}(X,Y;Z,T)\\Rightarrow C(X,Y) \\cong_t C(Z,T),\\ f \\mapsto ψ \\circ f \\circ φ^{-1}$$$
Lean4
/-- Any pair of homeomorphisms `X ≃ₜ Z` and `Y ≃ₜ T` gives rise to a homeomorphism
`C(X, Y) ≃ₜ C(Z, T)`. -/
protected def _root_.Homeomorph.arrowCongr (φ : X ≃ₜ Z) (ψ : Y ≃ₜ T) : C(X, Y) ≃ₜ C(Z, T)
where
toFun f := .comp ψ <| f.comp φ.symm
invFun f := .comp ψ.symm <| f.comp φ
left_inv f := ext fun _ ↦ ψ.left_inv (f _) |>.trans <| congrArg f <| φ.left_inv _
right_inv f := ext fun _ ↦ ψ.right_inv (f _) |>.trans <| congrArg f <| φ.right_inv _
continuous_toFun := continuous_postcomp _ |>.comp <| continuous_precomp _
continuous_invFun := continuous_postcomp _ |>.comp <| continuous_precomp _
