English
A pair of homeomorphisms e: X1 ≃t X2 and e': Y1 ≃t Y2 induces a bijection between continuous maps C(X1,Y1) ≃ C(X2,Y2) given by f ↦ e' ∘ f ∘ e⁻¹.
Русский
Пусть e: X1 ≃t X2 и e': Y1 ≃t Y2 — гомеоморфизмы; тогда функция от отображений f: X1→Y1 к e' ∘ f ∘ e⁻¹ задаёт биекцию между C(X1,Y1) и C(X2,Y2).
LaTeX
$$$C(X_1,Y_1) \simeq C(X_2,Y_2)\quad\text{via } f \mapsto e' \circ f \circ e^{-1}$$$
Lean4
/-- The bijection `C(X₁, Y₁) ≃ C(X₂, Y₂)` induced by homeomorphisms
`e : X₁ ≃ₜ X₂` and `e' : Y₁ ≃ₜ Y₂`. -/
@[simps]
def _root_.Homeomorph.continuousMapCongr {X₁ X₂ Y₁ Y₂ : Type*} [TopologicalSpace X₁] [TopologicalSpace X₂]
[TopologicalSpace Y₁] [TopologicalSpace Y₂] (e : X₁ ≃ₜ X₂) (e' : Y₁ ≃ₜ Y₂) : C(X₁, Y₁) ≃ C(X₂, Y₂)
where
toFun f := ContinuousMap.comp ⟨_, e'.continuous⟩ (f.comp ⟨_, e.symm.continuous⟩)
invFun g := ContinuousMap.comp ⟨_, e'.symm.continuous⟩ (g.comp ⟨_, e.continuous⟩)
left_inv _ := by aesop
right_inv _ := by aesop
