English
Currying provides a homeomorphism between the function spaces C(X × Y, Z) and C(X, C(Y, Z)) when X and Y are locally compact spaces.
Русский
Каррирование устанавливает гомеоморфизм между пространствами функций C(X × Y, Z) и C(X, C(Y, Z)) при локально компактных X и Y.
LaTeX
$$$C(X\\times Y, Z) \\simeq_t C(X, C(Y, Z))$$$
Lean4
/-- Currying as a homeomorphism between the function spaces `C(X × Y, Z)` and `C(X, C(Y, Z))`. -/
def curry [LocallyCompactSpace X] [LocallyCompactSpace Y] : C(X × Y, Z) ≃ₜ C(X, C(Y, Z)) :=
⟨⟨ContinuousMap.curry, uncurry, by intro; ext; rfl, by intro; ext; rfl⟩, continuous_curry, continuous_uncurry⟩
