sigmaFinsuppAddEquivPiFinsupp_apply

English

The apply form of the additive equivalence expresses that the coordinate of the image equals the corresponding component of the original.

Русский

Формула применения аддитивного эквивалентства выражает, что координата образа равна соответствующей компоненте исходного.

LaTeX

$$$\\sigmaFinsuppAddEquivPiFinsupp f j i = f j i$$$

Lean4

@[simp]
theorem sigmaFinsuppAddEquivPiFinsupp_apply {α : Type*} {ιs : η → Type*} [AddMonoid α] (f : (Σ j, ιs j) →₀ α) (j i) :
    sigmaFinsuppAddEquivPiFinsupp f j i = f ⟨j, i⟩ :=
  rfl

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