English
Let f be a family of lp(E, p) elements indexed by ι, and s a finite index set. The sum ∑ i∈s f(i), viewed as an lp-element, is computed coordinatewise; i.e., for every x, (∑ i∈s f(i))(x) = ∑ i∈s f(i)(x).
Русский
Пусть f — семейство элементов пространства lp(E, p), индексируемое по ι, и пусть s — конечный подмножество индексов. Сумма ∑ i∈s f(i), рассматриваемая как элемент lp(E, p), вычисляется по координатам: для каждого x выполняется (∑ i∈s f(i))(x) = ∑ i∈s f(i)(x).
LaTeX
$$$$ \forall x, \left(\sum_{i\in s} f(i)\right)(x) = \sum_{i\in s} f(i)(x). $$$$
Lean4
theorem coeFn_sum {ι : Type*} (f : ι → lp E p) (s : Finset ι) : ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i) := by simp
