English
A continuous function is strongly measurable when either the source space or the target space is second-countable.
Русский
Непрерывная функция является сильно измеримой, если либо источник, либо цель второсчётны.
LaTeX
$$$\text{Continuous}(f) \Rightarrow \text{StronglyMeasurable}(f)$, given that either the domain or codomain is second-countable.$$
Lean4
/-- A continuous function is strongly measurable when either the source space or the target space
is second-countable. -/
theorem _root_.Continuous.stronglyMeasurable [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α]
[TopologicalSpace β] [PseudoMetrizableSpace β] [h : SecondCountableTopologyEither α β] {f : α → β}
(hf : Continuous f) : StronglyMeasurable f := by
borelize β
cases h.out
· rw [stronglyMeasurable_iff_measurable_separable]
refine ⟨hf.measurable, ?_⟩
exact isSeparable_range hf
· exact hf.measurable.stronglyMeasurable
