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