English
A continuous function with compact support on a product space is strongly measurable with respect to the product sigma-algebra.
Русский
Непрерывная функция с компактной поддержкой на произведении пространств сильно измерима относительно произведенной сигма-алгебры.
LaTeX
$$$\text{Continuous}(f) \land \text{HasCompactSupport}(f) \Rightarrow \mathrm{StronglyMeasurable}(f)$$$
Lean4
/-- A continuous function with compact support on a product space is strongly measurable for the
product sigma-algebra. The subtlety is that we do not assume that the spaces are separable, so the
product of the Borel sigma algebras might not contain all open sets, but still it contains enough
of them to approximate compactly supported continuous functions. -/
theorem _root_.HasCompactSupport.stronglyMeasurable_of_prod {X Y : Type*} [Zero α] [TopologicalSpace X]
[TopologicalSpace Y] [MeasurableSpace X] [MeasurableSpace Y] [OpensMeasurableSpace X] [OpensMeasurableSpace Y]
[TopologicalSpace α] [PseudoMetrizableSpace α] {f : X × Y → α} (hf : Continuous f) (h'f : HasCompactSupport f) :
StronglyMeasurable f := by
borelize α
apply stronglyMeasurable_iff_measurable_separable.2 ⟨h'f.measurable_of_prod hf, ?_⟩
letI : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
exact IsCompact.isSeparable (s := range f) (h'f.isCompact_range hf)
