English
The currying operation provides a measurable bijection between functions of two arguments and curried functions; i.e., there is a measurable equivalence between (ι × κ → X) and (ι → κ → X).
Русский
Куррирование задаёт взаимно однозначное соответствие между функциями двум аргументам и крурированными функциями, причём это соответствие измеримо.
LaTeX
$$$(ι \\times κ \\to X) \\cong^{\\mathrm{meas}} (ι \\to κ \\to X).$$$
Lean4
/-- The currying operation `Sigma.curry` as a measurable equivalence.
See `MeasurableEquiv.piCurry` for the dependent version. -/
@[simps!]
def curry (ι κ X : Type*) [MeasurableSpace X] : (ι × κ → X) ≃ᵐ (ι → κ → X)
where
toEquiv := Equiv.curry ι κ X
measurable_toFun := by fun_prop
measurable_invFun := by fun_prop
