coe_curry — Mathlib

English

The underlying function of the curry measurable equivalence is the ordinary currying map.

Русский

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

LaTeX

$$$\operatorname{toFun}(\text{curry}_{ι κ X}) = \operatorname{Function.curry}.$$$

Lean4

theorem coe_curry (ι κ X : Type*) [MeasurableSpace X] : ⇑(curry ι κ X) = Function.curry :=
  rfl

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