Theorems · Theorem · measure theory

HasCompactSupport.measurable_of_prod

∀ {X : Type u_3} {Y : Type u_4} {α : Type u_5} [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 α]
  [inst_9 : MeasurableSpace α] [BorelSpace α] {f : X × Y → α}, Continuous f → HasCompactSupport f → Measurable f

A continuous function with compact support on a product space is 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.SimpleFuncDense

Cited by

1 results in Mathlib

Foundations

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

Assumes

ZeroTopologicalSpaceTopologicalSpaceMeasurableSpaceMeasurableSpaceOpensMeasurableSpaceOpensMeasurableSpaceTopologicalSpaceTopologicalSpace.PseudoMetrizableSpaceMeasurableSpaceBorelSpace