snd_sumFinsuppAddEquivProdFinsupp

English

Let f : α ⊕ β →₀ M. Under the additive equivalence sumFinsuppAddEquivProdFinsupp between α ⊕ β and (α →₀ M) × (β →₀ M), the second projection evaluated at y ∈ β equals f( Sum.inr y ).

Русский

Пусть f : α ⊕ β →₀ M. При помощи аддитивного эквивалента между α ⊕ β и (α →₀ M) × (β →₀ M) второй проекции при y ∈ β равна f( Sum.inr y ).

LaTeX

$$$(\\mathrm{sumFinsuppAddEquivProdFinsupp} f)_2(y) = f(\\mathrm{Sum.inr}\\, y)$$$

Lean4

theorem snd_sumFinsuppAddEquivProdFinsupp {α β : Type*} (f : α ⊕ β →₀ M) (y : β) :
    (sumFinsuppAddEquivProdFinsupp f).2 y = f (Sum.inr y) :=
  rfl

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