English
Let μ be a measure and T, T' be families of continuous linear maps dominated finitely additively by μ with constants C and C'. Then for any f : α → E, the value of setToFun at the sum T + T' equals the sum of the two corresponding setToFun values: setToFun μ (T + T') (hT.add hT') f = setToFun μ T hT f + setToFun μ T' hT' f. (If f is not integrable, both sides are interpreted according to the usual convention for undefined integrals.)
Русский
Пусть μ — мера на α, T и T' — семейства непрерывно-лыжных отображений, задаваемые на множества α и управляемые условием DominatedFinMeasAdditive с константами C и C'. Тогда для любого f : α → E выполняется равенство setToFun μ (T + T') (hT.add hT') f = setToFun μ T hT f + setToFun μ T' hT' f. (При неинтегрируемом f левая часть и правая трактуются согласно принятию нормы интеграла.)
LaTeX
$$$\\forall \\mu, T, T', h_T, h_{T'}, f:\\; \\mathrm{setToFun}(\\mu, T+T')\\,(h_T.add\, h_{T'})\,f = \\mathrm{setToFun}(\\mu, T)\\,h_T\,f + \\mathrm{setToFun}(\\mu, T')\\,h_{T'}\,f,$$$
Lean4
theorem setToFun_add_left (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (f : α → E) :
setToFun μ (T + T') (hT.add hT') f = setToFun μ T hT f + setToFun μ T' hT' f :=
by
by_cases hf : Integrable f μ
· simp_rw [setToFun_eq _ hf, L1.setToL1_add_left hT hT']
· simp_rw [setToFun_undef _ hf, add_zero]
