Theorems · Theorem · measure theory

Measurable.measure_of_isPiSystem_of_isProbabilityMeasure

∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : α → MeasureTheory.Measure β}
  [∀ (a : α), MeasureTheory.IsProbabilityMeasure (μ a)] {S : Set (Set β)},
  mβ = MeasurableSpace.generateFrom S → IsPiSystem S → (∀ s ∈ S, Measurable fun a => (μ a) s) → Measurable μ

Defined in

Mathlib.MeasureTheory.Measure.GiryMonad

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsProbabilityMeasure