Theorems · Theorem · measure theory

Measurable.measure_of_isPiSystem

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

Defined in

Mathlib.MeasureTheory.Measure.GiryMonad

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasure