English
Assume hT, hT', and hT'' are DominatedFinMeasAdditive for T, T', T'' and that on every measurable set s with finite μ-measure we have T''(s) = T(s) + T'(s). Then for any f, setToFun μ T'' hT'' f = setToFun μ T hT f + setToFun μ T' hT' f.
Русский
Пусть для T, T', T'' выполняются условия DominatedFinMeasAdditive, а на каждом измеримом множестве s с конечной мерой μ выполняется T''(s) = T(s) + T'(s). Тогда для любого f выполняется setToFun μ T'' hT'' f = setToFun μ T hT f + setToFun μ T' hT' f.
LaTeX
$$$\\forall h_T\\, h_{T'}\\, h_{T''},\\;\\forall f:\\; \\mathrm{setToFun}(\\mu, T'')\\,(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')
(hT'' : DominatedFinMeasAdditive μ T'' C'') (h_add : ∀ s, MeasurableSet s → μ s < ∞ → T'' s = T s + T' s)
(f : α → E) : setToFun μ T'' 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' hT'' h_add]
· simp_rw [setToFun_undef _ hf, add_zero]
