sigmaCurry_apply — Mathlib

English

For every f in the iterated direct sum, sigmaCurry recovers the original coordinate: sigmaCurry f i j = f(⟨i,j⟩).

Русский

Для любого элемента f в повторной прямой сумме вернется исходная координата: sigmaCurry f i j = f(⟨i,j⟩).

LaTeX

$$$$\\sigma\\text{-Curry}(f)(i,j) = f(\\langle i,j\\rangle).$$$$

Lean4

@[simp]
theorem sigmaCurry_apply (f : ⨁ i : Σ _i, _, δ i.1 i.2) (i : ι) (j : α i) : sigmaCurry f i j = f ⟨i, j⟩ :=
  DFinsupp.sigmaCurry_apply (δ := δ) _ i j

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