English
Let f be a bilinear map in the multilinear sense, taking a pair of index sets (ι, ι') to outputs in G'. For any function m : ι ⊕ ι' → G, the value of the uncurrySum of f at m equals applying f to the pair of arguments obtained by composing m with the left and right injections. In symbols, f.uncurrySum(m) = f(m ∘ Sum.inl, m ∘ Sum.inr).
Русский
Пусть f — билинейная по смыслу многолинейная карта, принимающая пару индексов (ι, ι') и выход в G'. Для любой функции m : ι ⊕ ι' → G значение uncurrySum(f) в m равно применению f к паре аргументов, полученных как m ∘ Sum.inl и m ∘ Sum.inr. Обозначим: f.uncurrySum(m) = f(m ∘ Sum.inl, m ∘ Sum.inr).
LaTeX
$$$\\forall f\\;\\forall m:\\, (\\iota \\oplus \\iota') \\to G,\\quad f.uncurrySum\\,m = f\\big(m \\circ Sum.inl\\big)\\big(m \\circ Sum.inr\\big).$$$
Lean4
@[simp]
theorem uncurrySum_apply
(f : ContinuousMultilinearMap 𝕜 (fun _ : ι => G) (ContinuousMultilinearMap 𝕜 (fun _ : ι' => G) G'))
(m : ι ⊕ ι' → G) : f.uncurrySum m = f (m ∘ Sum.inl) (m ∘ Sum.inr) :=
rfl
