sigmaFinsuppLEquivPiFinsupp_symm_apply

English

There is a canonical linear equivalence between finsupp on a sum of types (Σ j, ιs j) and a dependent function type j ↦ ιs j →₀ M.

Русский

Существует каноническое линейное эквивалентное отображение между Finsupp на сумме типов (Σ j, ιs j) и зависимой функцией j ↦ ιs j →₀ M.

LaTeX

$$$\sigmaFinsuppLEquivPiFinsupp: (\Sigma j, ιs j) \to_0 M \simeq_R (j : _) → (ιs j \to_0 M)$$$

Lean4

@[simp]
theorem sigmaFinsuppLEquivPiFinsupp_symm_apply {M : Type*} {ιs : η → Type*} [AddCommMonoid M] [Module R M]
    (f : (j : _) → (ιs j →₀ M)) (ji) : (Finsupp.sigmaFinsuppLEquivPiFinsupp R).symm f ji = f ji.1 ji.2 :=
  rfl

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