sumFinsuppEquivProdFinsupp_symm_inl

English

For fg ∈ (α →₀ γ) × (β →₀ γ) and x ∈ α, the inverse image under the canonical isomorphism sends Sum.inl x to the first component: (sumFinsuppEquivProdFinsupp.symm fg)(Sum.inl x) = fg.1 x.

Русский

Для fg ∈ (α →₀ γ) × (β →₀ γ) и x ∈ α обратное отображение через каноническое отображение отправляет Sum.inl x в первую компоненту: (sumFinsuppEquivProdFinsupp.symm fg)(Sum.inl x) = fg.1 x.

LaTeX

$$$(\\mathrm{sumFinsuppEquivProdFinsupp}.\\mathrm{symm}\\; fg)(\\mathrm{Sum.inl}\\, x) = fg.1\\, x$$$

Lean4

theorem sumFinsuppEquivProdFinsupp_symm_inl {α β γ : Type*} [Zero γ] (fg : (α →₀ γ) × (β →₀ γ)) (x : α) :
    (sumFinsuppEquivProdFinsupp.symm fg) (Sum.inl x) = fg.1 x :=
  rfl

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