fst_sumFinsuppLEquivProdFinsupp — Mathlib

English

The first coordinate map under the sum-to-product equivalence is given by the left projection.

Русский

Первая координата под отображением эквивалентности между суммой и произведением соответствует левой проекции.

LaTeX

$$$(\text{sumFinsuppLEquivProdFinsupp } R\ f).1\ x = f (\mathrm{Sum}.inl\ x)$$$

Lean4

theorem fst_sumFinsuppLEquivProdFinsupp {α β : Type*} (f : α ⊕ β →₀ M) (x : α) :
    (sumFinsuppLEquivProdFinsupp R f).1 x = f (Sum.inl x) :=
  rfl

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