English
If f is continuous on a set K and μ is locally finite, then f is locally integrable on K with respect to μ.
Русский
Если f непрерывна на множество K и μ локально конечна, то f локально интегрируема на K по μ.
LaTeX
$$$\operatorname{ContinuousOn}(f, K) \Rightarrow \operatorname{LocallyIntegrableOn}(f, K, \mu)$$$
Lean4
/-- A function `f` continuous on a compact set `K` is integrable on this set with respect to any
locally finite measure. -/
theorem integrableOn_compact' (hK : IsCompact K) (h'K : MeasurableSet K) (hf : ContinuousOn f K) : IntegrableOn f K μ :=
by
refine ⟨ContinuousOn.aestronglyMeasurable_of_isCompact hf hK h'K, ?_⟩
have : Fact (μ K < ∞) := ⟨hK.measure_lt_top⟩
obtain ⟨C, hC⟩ : ∃ C, ∀ x ∈ f '' K, ‖x‖ ≤ C := IsBounded.exists_norm_le (hK.image_of_continuousOn hf).isBounded
apply HasFiniteIntegral.of_bounded (C := C)
filter_upwards [ae_restrict_mem h'K] with x hx using hC _ (mem_image_of_mem f hx)
