Theorems · Theorem · measure theory

MeasureTheory.ProbabilityMeasure.continuous_prod

∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β] [inst_2 : TopologicalSpace α]
  [inst_3 : TopologicalSpace β] [SecondCountableTopology α] [inst_5 : SecondCountableTopology β]
  [TopologicalSpace.PseudoMetrizableSpace α] [TopologicalSpace.PseudoMetrizableSpace β]
  [inst_8 : OpensMeasurableSpace α] [inst_9 : OpensMeasurableSpace β], Continuous fun μ => μ.1.prod μ.2

The map associating to two probability measures their product is a continuous map.

Defined in

Mathlib.MeasureTheory.Measure.FiniteMeasureProd

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpaceTopologicalSpaceTopologicalSpaceSecondCountableTopologySecondCountableTopologyTopologicalSpace.PseudoMetrizableSpaceTopologicalSpace.PseudoMetrizableSpaceOpensMeasurableSpaceOpensMeasurableSpace