Theorem MeasureTheory.measure_preimage_fst_singleton_eq_tsum

Modification history

2024-11-03 19:16
Mathlib/MeasureTheory/Measure/NullMeasurable.lean
feat: `μ (Prod.fst ⁻¹' {x}) = ∑' y, μ {(x, y)}` (#18390) …
Added MeasureTheory.measure_preimage_fst_singleton_eq_tsumView on Github →