English
If a function is continuous on a set s and s is measurable, and s is separable in the sense of topology, then f is AEStronglyMeasurable w.r.t. μ.restrict s.
Русский
Если функция непрерывна на s и s измеримо, и s сепарируемо, то f является AEStronglyMeasurable относительно μ.restrict s.
LaTeX
$$$\\text{AEStronglyMeasurable } f (\\mu \\restriction s)$$$
Lean4
/-- A function which is continuous on a set `s` is almost everywhere strongly measurable with
respect to `μ.restrict s` when either the source space or the target space is second-countable. -/
theorem aestronglyMeasurable [TopologicalSpace α] [TopologicalSpace β] [h : SecondCountableTopologyEither α β]
[OpensMeasurableSpace α] [PseudoMetrizableSpace β] {f : α → β} {s : Set α} {μ : Measure α} (hf : ContinuousOn f s)
(hs : MeasurableSet s) : AEStronglyMeasurable f (μ.restrict s) :=
by
borelize β
refine
aestronglyMeasurable_iff_aemeasurable_separable.2
⟨hf.aemeasurable hs, f '' s, ?_, mem_of_superset (self_mem_ae_restrict hs) (subset_preimage_image _ _)⟩
cases h.out
· rw [image_eq_range]
exact isSeparable_range <| continuousOn_iff_continuous_restrict.1 hf
· exact .of_separableSpace _
