measurable_curry — Mathlib

English

The curry transformation is a measurable map between function spaces; the map that curries a function is measurable.

Русский

Преобразование карри является измеримым отображением между пространствами функций; отображение карри измеримо.

LaTeX

$$$ \text{measurable\_curry} : Measurable (\text{Function.curry}) $$$

Lean4

@[fun_prop, measurability]
theorem measurable_curry : Measurable (@curry ι κ X) :=
  measurable_pi_lambda _ fun _ ↦
    measurable_pi_lambda _ fun _ ↦
      measurable_pi_apply
        _
          -- This cannot be tagged with `fun_prop` because `fun_prop` can see through `Function.uncurry`.

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