English
Sum over a Finset of indices of a family of ContinuousMultilinearMaps applied to a fixed m equals the Finset sum of the evaluations.
Русский
Сумма по конечному множеству индексов семейства отображений равна сумме значений для фиксированного m.
LaTeX
$$$\\sum_{a \\in s} f(a)\\, m = \\sum_{a \\in s} (f(a))\\, m$$$
Lean4
/-- The natural equivalence between continuous linear maps from `M₂` to `M₃`
and continuous 1-multilinear maps from `M₂` to `M₃`. -/
@[simps! apply_toMultilinearMap apply_apply symm_apply_apply]
def ofSubsingleton [Subsingleton ι] (i : ι) : (M₂ →L[R] M₃) ≃ ContinuousMultilinearMap R (fun _ : ι => M₂) M₃
where
toFun f := ⟨MultilinearMap.ofSubsingleton R M₂ M₃ i f, (map_continuous f).comp (continuous_apply i)⟩
invFun
f :=
⟨(MultilinearMap.ofSubsingleton R M₂ M₃ i).symm f.toMultilinearMap,
(map_continuous f).comp <| continuous_pi fun _ ↦ continuous_id⟩
right_inv
f := toMultilinearMap_injective <| (MultilinearMap.ofSubsingleton R M₂ M₃ i).apply_symm_apply f.toMultilinearMap
