Theorems · Theorem · probability

ProbabilityTheory.HasLaw.comp

∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω} {𝓨 : Type u_3} {m𝓨 : MeasurableSpace 𝓨}
  {ν : MeasureTheory.Measure 𝓨} {Y : 𝓧 → 𝓨},
  ProbabilityTheory.HasLaw Y ν μ → ProbabilityTheory.HasLaw X μ P → ProbabilityTheory.HasLaw (Y ∘ X) ν P

Defined in

Mathlib.Probability.HasLaw

Cited by

12 results in Mathlib

Foundations

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