English
If f is integrable and fs_i are approximations converging in L1, then setToFun μ T hT (fs_i) converges to setToFun μ T hT f.
Русский
Если f интегрируема и fs_i сходятся в L1 приближениями, то setToFun μ T hT(fs_i) сходится к setToFun μ T hT(f).
LaTeX
$$$\\text{Tendsto} (fs_i) \\to f \\Rightarrow \\text{Tendsto} (setToFun\\, μ\\, T\\, hT\\, fs_i) \\to setToFun\\, μ\\, T\\, hT\\, f.$$$
Lean4
theorem setToL1_congr_left' (T T' : Set α → E →L[ℝ] F) {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C)
(hT' : DominatedFinMeasAdditive μ T' C') (h : ∀ s, MeasurableSet s → μ s < ∞ → T s = T' s) (f : α →₁[μ] E) :
setToL1 hT f = setToL1 hT' f := by
suffices setToL1 hT = setToL1 hT' by rw [this]
refine ContinuousLinearMap.extend_unique (setToL1SCLM α E μ hT) _ _ _ _ ?_
ext1 f
suffices setToL1 hT' f = setToL1SCLM α E μ hT f by rw [← this]; simp [coeToLp]
rw [setToL1_eq_setToL1SCLM]
exact (setToL1SCLM_congr_left' hT hT' h f).symm
