piCurry_apply — Mathlib

English

For α as above, the linear equivalence piCurry sends a function f to its curried form; namely, piCurry(R, α) f equals Sigma.curry f.

Русский

Для заданного α каррированная форма функции f получают линейным эквивалентом piCurry; то есть piCurry(R, α) f равно Sigma.curry f.

LaTeX

$$$$\\pi\\text{Curry}(R, \\alpha)\\, f = \\Sigma\\text{curry} \\; f,$$$$

Lean4

@[simp]
theorem piCurry_apply {ι : Type*} {κ : ι → Type*} (α : ∀ i, κ i → Type*) [∀ i k, AddCommMonoid (α i k)]
    [∀ i k, Module R (α i k)] (f : ∀ x : Σ i, κ i, α x.1 x.2) : piCurry R α f = Sigma.curry f :=
  rfl

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