sumArrowEquivProdArrow — Mathlib

English

There is a ring isomorphism between the function space from α ⊕ β to R and the product of function spaces α → R and β → R, given by decomposing a function on a disjoint union into its restrictions.

Русский

Существует изоморфизм колец между множеством функций от α ⊕ β в R и произведением функций α → R и β → R, даваемый разложением функции по сумме на её ограничения.

LaTeX

$$$ (\alpha \oplus \beta \to R) \cong_{+*} (\alpha \to R) \times (\beta \to R) $$$

Lean4

/-- `Equiv.sumArrowEquivProdArrow` as a ring isomorphism. -/
def sumArrowEquivProdArrow : (α ⊕ β → R) ≃+* (α → R) × (β → R)
    where
  __ := Equiv.sumArrowEquivProdArrow α β R
  map_mul' _ _ := rfl
  map_add' _ _ := rfl

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