Theorems · Theorem · measure theory

MeasureTheory.measure_preimage_fst_singleton_eq_tsum

∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSingletonClass α] {mβ : MeasurableSpace β}
  [MeasurableSingletonClass β] [Countable β] (μ : MeasureTheory.Measure (α × β)) (x : α),
  μ (Prod.fst ⁻¹' {x}) = ∑' (y : β), μ {(x, y)}

Defined in

Mathlib.MeasureTheory.Measure.NullMeasurable

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSingletonClassMeasurableSingletonClassCountable