sumFinsuppAddEquivProdFinsupp_symm_inl

English

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

Русский

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

LaTeX

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

Lean4

theorem sumFinsuppAddEquivProdFinsupp_symm_inl {α β : Type*} (fg : (α →₀ M) × (β →₀ M)) (x : α) :
    (sumFinsuppAddEquivProdFinsupp.symm fg) (Sum.inl x) = fg.1 x :=
  rfl

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