Theorems · Theorem · measure theory

MeasureTheory.ProbabilityMeasure.measurable_fun_prod

∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β],
  Measurable fun μ => (↑μ.1).prod ↑μ.2

The monoidal product is a measurable function from the product of probability spaces over α and β into the type of probability spaces over α × β. Lemma 4.1 of [A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics][fritz2020].

Defined in

Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpace