English
If a family of α → E is integrable with a limit f in L1, and fs_i converge to f in L1, then setToFun μ T hT (fs_i) tends to setToFun μ T hT f.
Русский
Если последовательность функций в L1 сходится к f, то значения setToFun сходятся к setToFun(f).
LaTeX
$$$\text{If } (f_i)\to_{L^1} f,\; \mathrm{setToFun}(\mu, T)\,h_T\,(f_i) \to \mathrm{setToFun}(\mu, T)\,h_T\,f$$$
Lean4
theorem setToFun_congr_ae (hT : DominatedFinMeasAdditive μ T C) (h : f =ᵐ[μ] g) :
setToFun μ T hT f = setToFun μ T hT g := by
by_cases hfi : Integrable f μ
· have hgi : Integrable g μ := hfi.congr h
rw [setToFun_eq hT hfi, setToFun_eq hT hgi, (Integrable.toL1_eq_toL1_iff f g hfi hgi).2 h]
· have hgi : ¬Integrable g μ := by rw [integrable_congr h] at hfi; exact hfi
rw [setToFun_undef hT hfi, setToFun_undef hT hgi]
