English
If s_i are compact sets forming a countable cover of X and the summability condition on the restricted norms holds, then the continuous function f is integrable on the union of the s_i.
Русский
Если s_i — счетное покрытие X компактами и выполняется условие суммируемости норм ограничений, то непрерывная функция f интегрируема на объединении s_i.
LaTeX
$$$$\\text{Integrable}(f, \\bigcup_i s_i)$$ under summability.$$
Lean4
/-- If `s` is a countable family of compact sets covering `X`, `f` is a continuous function, and
the sequence `‖f.restrict (s i)‖ * μ (s i)` is summable, then `f` is integrable. -/
theorem integrable_of_summable_norm_restrict {f : C(X, E)} {s : ι → Compacts X}
(hf : Summable fun i : ι => ‖f.restrict (s i)‖ * μ.real (s i)) (hs : ⋃ i : ι, ↑(s i) = (univ : Set X)) :
Integrable f μ := by simpa only [hs, integrableOn_univ] using integrableOn_iUnion_of_summable_norm_restrict hf
