English
Let X be a topological space with the discrete topology. Then every function X → Y is continuous, so the space of continuous maps C(X, Y) (with the compact-open topology) is topologically the same as the full function space Y^X (with the product topology). In particular there exists a canonical homeomorphism between C(X, Y) and Y^X.
Русский
Пусть X обладает дискретной топологией. Тогда каждая функция X → Y непрерывна, поэтому пространство непрерывных отображений C(X, Y) с компактно-открытой топологией гомеоморфно пространству всех функций Y^X (с произведением топологий). Существует каноническое гомеоморфизм между C(X, Y) и Y^X.
LaTeX
$$$C(X,Y) \cong_{\mathrm{Homeo}} Y^{X} \quad \text{when } X \text{ is discrete}$$$
Lean4
/-- The continuous functions from `X` to `Y` are the same as the plain functions when `X` is
discrete. -/
@[simps toEquiv]
def homeoFnOfDiscrete : C(X, Y) ≃ₜ (X → Y) where
__ := equivFnOfDiscrete
continuous_invFun := continuous_compactOpen.2 fun K hK U hU ↦ isOpen_set_pi hK.finite_of_discrete fun _ _ ↦ hU
