Theorems · Theorem · probability

ProbabilityTheory.HasLaw.map_eq

∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.HasLaw._auto_1},
  ProbabilityTheory.HasLaw X μ P → MeasureTheory.Measure.map X P = μ

Defined in

Mathlib.Probability.HasLaw

Cited by

31 results in Mathlib

Foundations

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