sumArrowLequivProdArrow_apply_fst

English

There is a linear equivalence between functions on the sum α ⊕ β and the pair of functions α → M and β → M.

Русский

Существует линейное эквивалентство между функциями на сумме α ⊕ β и парой функций α → M и β → M.

LaTeX

$$$$ (\\alpha \\oplus \\beta \\to M) \\cong_{\\!R} (\\alpha \\to M) \\times (\\beta \\to M), $$$$

Lean4

@[simp]
theorem sumArrowLequivProdArrow_apply_fst {α β} (f : α ⊕ β → M) (a : α) :
    (sumArrowLequivProdArrow α β R M f).1 a = f (Sum.inl a) :=
  rfl

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