precompHomeomorph — Mathlib

English

If A ≅ B, then Hom(A, R) is homeomorphic to Hom(B, R).

Русский

Если A изоморфно B, то Hom(A, R) гомеоморфно Hom(B, R).

LaTeX

$$$\text{precompHomeomorph}(f): (B \to R) \simeq_t (A \to R)\quad \text{for } f: A \cong B$$$

Lean4

/-- If `A ≅ B`, then `Hom(A, R)` is homeomorphic to `Hom(B, R)`. -/
@[simps]
def precompHomeomorph (f : A ≅ B) : (B ⟶ R) ≃ₜ (A ⟶ R)
    where
  toFun φ := _
  invFun φ := _
  continuous_toFun := continuous_precomp f.hom
  continuous_invFun := continuous_precomp f.inv
  left_inv _ := by simp
  right_inv _ := by simp

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