English
Let f be a finitely supported function on α ⊕ β with values in γ. Under the canonical decomposition of finitely supported functions, the second component corresponds to the restriction to β, so for every y ∈ β, the second coordinate evaluated at y equals f evaluated at the injection of y into α ⊕ β: f(inr y).
Русский
Пусть f — конечноподдерживаемая функция от α ⊕ β в γ. При каноническом разложении конечноподдерживаемых функций второе слагаемое соответствует ограничению на β, потому для каждого y ∈ β выполняется (второй компонент) при y равенству f(inr y).
LaTeX
$$$(\\mathrm{sumFinsuppEquivProdFinsupp} f)_2(y) = f(\\mathrm{Sum.inr}\\, y)$$$
Lean4
theorem snd_sumFinsuppEquivProdFinsupp {α β γ : Type*} [Zero γ] (f : α ⊕ β →₀ γ) (y : β) :
(sumFinsuppEquivProdFinsupp f).2 y = f (Sum.inr y) :=
rfl
