fst_sumFinsuppAddEquivProdFinsupp

English

Let f be a finitely supported function on α ⊕ β with values in M. Under the additive equivalence with (α →₀ M) × (β →₀ M), the first projection corresponds to the restriction to α: (sumFinsuppAddEquivProdFinsupp f).1 x = f( Sum.inl x ).

Русский

Пусть f — конечноподдерживаемая функция на α ⊕ β в M. При переходе к паре (α →₀ M) × (β →₀ M) первая компонента равна ограничению к α: (sumFinsuppAddEquivProdFinsupp f).1 x = f( Sum.inl x ).

LaTeX

$$$(\\mathrm{sumFinsuppAddEquivProdFinsupp} f)_1(x) = f(\\mathrm{Sum.inl}\\, x)$$$

Lean4

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

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