piCurry_symm_apply — Mathlib

English

The inverse of the piCurry is the uncurry operation: (piCurry(R, α)).symm f equals Sigma.uncurry f.

Русский

Обратное к piCurry — это uncurry: (piCurry(R, α)).symm f = Sigma.uncurry f.

LaTeX

$$$$ (\\pi\\text{Curry}(R, \\alpha))^{-1} \\; f = \\Sigma\\text{uncurry} \\; f, $$$$

Lean4

@[simp]
theorem piCurry_symm_apply {ι : Type*} {κ : ι → Type*} (α : ∀ i, κ i → Type*) [∀ i k, AddCommMonoid (α i k)]
    [∀ i k, Module R (α i k)] (f : ∀ a b, α a b) : (piCurry R α).symm f = Sigma.uncurry f :=
  rfl

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