English
Currying converts a map f: X×Y → Z to a map X → C(Y,Z); it is continuous in the compact-open topology under mild hypotheses.
Русский
Каррирование переводит отображение f: X×Y → Z в отображение X → C(Y,Z); при некоторых условиях это отображение непрерывно в компактно-открытой топологии.
LaTeX
$$$\text{curry}: C(X\times Y, Z) \to C(X, C(Y,Z))$$$
Lean4
/-- The curried form of a continuous map `α × β → γ` as a continuous map `α → C(β, γ)`.
If `a × β` is locally compact, this is continuous. If `α` and `β` are both locally
compact, then this is a homeomorphism, see `Homeomorph.curry`. -/
def curry (f : C(X × Y, Z)) : C(X, C(Y, Z))
where
toFun a := ⟨Function.curry f a, f.continuous.comp <| by fun_prop⟩
continuous_toFun := (continuous_postcomp f).comp continuous_coev
