sumFinsuppLEquivProdFinsupp_symm_inl

English

The inverse under the symmetrized equivalence sends the left injection coordinate back to the left component.

Русский

Обратное преобразование разворачивает левую инъекцию обратно к левой компоненте.

LaTeX

$$((sumFinsuppLEquivProdFinsupp R).symm f) (Sum.inl x) = f.1 x$$

Lean4

theorem sumFinsuppLEquivProdFinsupp_symm_inl {α β : Type*} (fg : (α →₀ M) × (β →₀ M)) (x : α) :
    ((sumFinsuppLEquivProdFinsupp R).symm fg) (Sum.inl x) = fg.1 x :=
  rfl

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