English
If f is continuous on s and s is NullMeasurableSet with respect to μ, then f is almost everywhere measurable with μ.restrict s.
Русский
Если f непрерывна на s и s является нулевой измеримой по отношению к μ, тогда f почти всюду измерима относительно μ.restrict s.
LaTeX
$$$\\text{AEMeasurable } f \\, (\\mu \\restriction s)$ under the hypothesis that $s$ is NullMeasurableSet w.r.t. μ.$$
Lean4
theorem aemeasurable₀ [TopologicalSpace α] [OpensMeasurableSpace α] [MeasurableSpace β] [TopologicalSpace β]
[BorelSpace β] {f : α → β} {s : Set α} {μ : Measure α} (hf : ContinuousOn f s) (hs : NullMeasurableSet s μ) :
AEMeasurable f (μ.restrict s) :=
by
rcases hs.exists_measurable_subset_ae_eq with ⟨t, ts, ht, t_eq_s⟩
rw [← Measure.restrict_congr_set t_eq_s]
exact ContinuousOn.aemeasurable (hf.mono ts) ht
