English
There is a natural equivalence between finsupps on a disjoint sum and pairs of finsupps: (α ⊕ β) →₀ γ ≃ (α →₀ γ) × (β →₀ γ).
Русский
Существует естественное эквивалентное соответствие между концевыми поддерживаемыми функциями на дизъюнктном сумме и парами таких функций: (α ⊕ β) →₀ γ ≃ (α →₀ γ) × (β →₀ γ).
LaTeX
$$$(\alpha \oplus \beta) \to_0 \gamma \;\simeq\; (\alpha \to_0 \gamma) \times (\beta \to_0 \gamma)$$$
Lean4
/-- `finsuppProdEquiv` defines the `Equiv` between `((α × β) →₀ M)` and `(α →₀ (β →₀ M))` given by
currying and uncurrying. -/
@[simps]
def finsuppProdEquiv : (α × β →₀ M) ≃ (α →₀ β →₀ M)
where
toFun := Finsupp.curry
invFun := Finsupp.uncurry
left_inv := uncurry_curry
right_inv := curry_uncurry
