sigmaLcurry_apply — Mathlib

English

For any f in the big direct sum, and any i and j, the value at the index (i, j) of sigmaLcurry R f is exactly f at ⟨i, j⟩.

Русский

Для любого f в большой прямой сумме и любых i, j значение в индексе (i, j) карри-отображения равно f при индексе ⟨i, j⟩.

LaTeX

$$$\sigma_{\mathrm{Lcurry}} R f \, \langle i,j \rangle = f \langle i,j \rangle.$$$

Lean4

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

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