sumFinsuppEquivProdFinsupp_symm_inr

English

For fg ∈ (α →₀ γ) × (β →₀ γ) and y ∈ β, the inverse image under the canonical isomorphism sends Sum.inr y to the second component: (sumFinsuppEquivProdFinsupp.symm fg)(Sum.inr y) = fg.2 y.

Русский

Для fg ∈ (α →₀ γ) × (β →₀ γ) и y ∈ β, обратное отображение отправляет Sum.inr y во вторую компоненту: (sumFinsuppEquivProdFinsupp.symm fg)(Sum.inr y) = fg.2 y.

LaTeX

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

Lean4

theorem sumFinsuppEquivProdFinsupp_symm_inr {α β γ : Type*} [Zero γ] (fg : (α →₀ γ) × (β →₀ γ)) (y : β) :
    (sumFinsuppEquivProdFinsupp.symm fg) (Sum.inr y) = fg.2 y :=
  rfl

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