snd_sumFinsuppLEquivProdFinsupp — Mathlib

English

The second coordinate map under the sum-to-product equivalence is given by the right projection.

Русский

Вторая координата под эквивалентностью равна правой проекции.

LaTeX

$$$(\text{sumFinsuppLEquivProdFinsupp } R\ f).2\ y = f (\mathrm{Sum}.inr\ y)$$$

Lean4

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

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