Strong measurability using second countability of the source.
theorem
Continuous.aestronglyMeasurable_of_secondCountable
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace α]
[OpensMeasurableSpace α]
[SecondCountableTopology α]
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : Continuous f)
:
A continuous map on a second-countable source is almost everywhere strongly measurable. Specifying the source avoids a search for second countability of the codomain.