English
If T' equals c times T on finite-measure measurable sets s (i.e., T'(s) = c•T(s)), then for all f, setToFun μ T' hT' f = c • setToFun μ T hT f.
Русский
Если T'(s) = c·T(s) для всех измеримых множеств s с конечной мерой, то для любого f выполняется setToFun μ T' hT' f = c·setToFun μ T hT f.
LaTeX
$$$\\forall c, \\forall f:\\; \\mathrm{setToFun}(\\mu, T')\\,(h_{T'})\,f = c\\cdot \\mathrm{setToFun}(\\mu, T)\\,h_T\,f$$$
Lean4
theorem setToFun_smul_left' (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (c : ℝ)
(h_smul : ∀ s, MeasurableSet s → μ s < ∞ → T' s = c • T s) (f : α → E) :
setToFun μ T' hT' f = c • setToFun μ T hT f :=
by
by_cases hf : Integrable f μ
· simp_rw [setToFun_eq _ hf, L1.setToL1_smul_left' hT hT' c h_smul]
· simp_rw [setToFun_undef _ hf, smul_zero]
