Theorems · Theorem · measure theory

MeasureTheory.Measure.ae_mem_finset_iff_map_eq_sum_dirac

∀ {α : Type u_4} {β : Type u_5} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSingletonClass α]
  {f : β → α} {s : Finset α} {μ : MeasureTheory.Measure β},
  AEMeasurable f μ →
    ((∀ᵐ (b : β) ∂μ, f b ∈ s) ↔ MeasureTheory.Measure.map f μ = ∑ a ∈ s, μ (f ⁻¹' {a}) • MeasureTheory.Measure.dirac a)

Defined in

Mathlib.MeasureTheory.Measure.Dirac

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSingletonClass