Theorems · Theorem · measure theory

HasCompactSupport.stronglyMeasurable_of_prod

∀ {α : Type u_1} {X : Type u_5} {Y : Type u_6} [inst : Zero α] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : MeasurableSpace X] [inst_4 : MeasurableSpace Y] [OpensMeasurableSpace X]
  [OpensMeasurableSpace Y] [inst_7 : TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α] {f : X × Y → α},
  Continuous f → HasCompactSupport f → MeasureTheory.StronglyMeasurable f

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.

Defined in

Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Cited by

1 results in Mathlib

Foundations

Depth 165 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

ZeroTopologicalSpaceTopologicalSpaceMeasurableSpaceMeasurableSpaceOpensMeasurableSpaceOpensMeasurableSpaceTopologicalSpaceTopologicalSpace.PseudoMetrizableSpace