sigmaFinsuppEquivDFinsupp_symm_apply

English

As above, the symmetric map applied to f at s gives f(s.1)(s.2).

Русский

Как и выше, для симметричного отображения f в точке s получается f(s.1)(s.2).

LaTeX

$$$(\\sigmaFinsuppEquivDFinsupp.symm f) s = f\,s.1\,s.2$$$

Lean4

@[simp]
theorem sigmaFinsuppEquivDFinsupp_symm_apply [Zero N] (f : Π₀ i, η i →₀ N) (s : Σ i, η i) :
    (sigmaFinsuppEquivDFinsupp.symm f : (Σ i, η i) →₀ N) s = f s.1 s.2 :=
  rfl

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