English
For a finite index set s and integrable f_i for each i∈s, the value of setToFun on the sum of functions f_i equals the sum of setToFun applied to each f_i.
Русский
Для конечного множества индексов s и интегрируемых f_i для каждого i ∈ s, значение setToFun на сумму функций равняется сумме setToFun от каждой f_i.
LaTeX
$$$\forall s : Finset I, \forall (f : I \to α \to E),\; (\forall i ∈ s, Integrable (f i) μ) \Rightarrow setToFun(μ, T, hT)(\sum i ∈ s, f i) = \sum i ∈ s, setToFun(μ, T, hT)(f i)$$$
Lean4
theorem setToFun_add (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ) (hg : Integrable g μ) :
setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT g := by
rw [setToFun_eq hT (hf.add hg), setToFun_eq hT hf, setToFun_eq hT hg, Integrable.toL1_add, (L1.setToL1 hT).map_add]
