uncurry — Mathlib

English

The curry map is continuous from C(X×Y,Z) to C(X, C(Y,Z)) when X×Y is locally compact.

Русский

Отображение каррирования непрерывно с C(X×Y,Z) в C(X, C(Y,Z)) при локально компактной паре X×Y.

LaTeX

$$$\text{curry}: C(X\times Y, Z) \to C(X, C(Y,Z))$ is continuous$$

Lean4

/-- The uncurried form of a continuous map `X → C(Y, Z)` as a continuous map `X × Y → Z` (if `Y` is
locally compact). If `X` is also locally compact, then this is a homeomorphism between the two
function spaces, see `Homeomorph.curry`. -/
@[simps]
def uncurry [LocallyCompactSpace Y] (f : C(X, C(Y, Z))) : C(X × Y, Z) :=
  ⟨_, continuous_uncurry_of_continuous f⟩

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