Theorems · Definition · measure theory

MeasureTheory.Measure.snd

{α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] → [inst_1 : MeasurableSpace β] → MeasureTheory.Measure (α × β) → MeasureTheory.Measure β

Marginal measure on β obtained from a measure on ρ α × β, defined by ρ.map Prod.snd.

Defined in

Mathlib.MeasureTheory.Measure.Prod

Cited by

21 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpace