sumFinsuppAddEquivProdFinsupp_symm_inr

English

For fg ∈ (α →₀ M) × (β →₀ M) and y ∈ β, the inverse image under the symm of sumFinsuppAddEquivProdFinsupp sends Sum.inr y to fg.2 y.

Русский

Для fg ∈ (α →₀ M) × (β →₀ M) и y ∈ β, обратное отображение через симм суммы-Finsupp-аддитивного эквивалента отправляет Sum.inr y во вторую компоненту fg.2 y.

LaTeX

$$$(\\mathrm{sumFinsuppAddEquivProdFinsupp}.\\mathrm{symm}}\\; fg)(\\mathrm{Sum.inr}\\, y) = fg.2\\, y$$$

Lean4

theorem sumFinsuppAddEquivProdFinsupp_symm_inr {α β : Type*} (fg : (α →₀ M) × (β →₀ M)) (y : β) :
    (sumFinsuppAddEquivProdFinsupp.symm fg) (Sum.inr y) = fg.2 y :=
  rfl

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