English
Under the same dominated finiteness hypotheses as above, but with the additional assumption that the range of f together with 0 is contained in a separable set s, the same approximation sequence converges to setToFun f without requiring a specific y0.
Русский
Пусть те же условия ограниченного суммирования выполняются, а дополнительно множество значений функции f вместе с 0 вложено в сепарабельное множество s. Тогда та же последовательность приближений сходится к setToFun f без явного выбора y0.
LaTeX
$$$\\operatorname{Tendsto}\\left( n \\mapsto \\operatorname{setToFun} \\;\\mu\\; T\\; hT\\; (\\mathrm{SimpleFunc.approxOn} \\ f \\ fmeas \\ s \\ 0 \\ (hs \\lvert\\ to by simp) \\ n)\\right)_{atTop} (\\nhds (\\operatorname{setToFun} \\;\\mu\\; T\\; hT\\; f))$$$
Lean4
theorem tendsto_setToFun_approxOn_of_measurable_of_range_subset (hT : DominatedFinMeasAdditive μ T C)
[MeasurableSpace E] [BorelSpace E] {f : α → E} (fmeas : Measurable f) (hf : Integrable f μ) (s : Set E)
[SeparableSpace s] (hs : range f ∪ {0} ⊆ s) :
Tendsto (fun n => setToFun μ T hT (SimpleFunc.approxOn f fmeas s 0 (hs <| by simp) n)) atTop
(𝓝 <| setToFun μ T hT f) :=
by
refine tendsto_setToFun_approxOn_of_measurable hT hf fmeas ?_ _ (integrable_zero _ _ _)
exact Eventually.of_forall fun x => subset_closure (hs (Set.mem_union_left _ (mem_range_self _)))
