sigmaUncurry_apply — Mathlib

English

For a direct sum object f in DirectSum, the uncurry map evaluated at (i,j) yields the component f i j; i.e., the coefficient at the index pair is exactly the corresponding component.

Русский

Для объекта DirectSum приложенная к нему функция sigmaUncurry на паре (i,j) даёт компоненту f i j.

LaTeX

$$$ \sigmaUncurry f \langle i,j \rangle = f i j $$$

Lean4

@[simp]
theorem sigmaUncurry_apply (f : ⨁ (i) (j), δ i j) (i : ι) (j : α i) : sigmaUncurry f ⟨i, j⟩ = f i j :=
  DFinsupp.sigmaUncurry_apply f i j

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