English
If f is continuous on a compact set s, then f is almost everywhere strongly measurable with respect to μ.restrict s.
Русский
Если функция непрерывна на компактном множестве s, то она почти везде сильно измерима относительно μ.restrict s.
LaTeX
$$$\\text{AEStronglyMeasurable } f (\\mu \\restriction s)$, when $s$ is compact and measurable.$$
Lean4
/-- A function which is continuous on a compact set `s` is almost everywhere strongly measurable
with respect to `μ.restrict s`. -/
theorem aestronglyMeasurable_of_isCompact [TopologicalSpace α] [OpensMeasurableSpace α] [TopologicalSpace β]
[PseudoMetrizableSpace β] {f : α → β} {s : Set α} {μ : Measure α} (hf : ContinuousOn f s) (hs : IsCompact s)
(h's : MeasurableSet s) : AEStronglyMeasurable f (μ.restrict s) :=
by
letI := pseudoMetrizableSpacePseudoMetric β
borelize β
rw [aestronglyMeasurable_iff_aemeasurable_separable]
refine ⟨hf.aemeasurable h's, f '' s, ?_, ?_⟩
· exact (hs.image_of_continuousOn hf).isSeparable
· exact mem_of_superset (self_mem_ae_restrict h's) (subset_preimage_image _ _)
