Mathlib v3 is deprecated. Go to Mathlib v4

Theorem measure_theory.lintegral_singleton

Modification history

2022-06-01 15:09
src/measure_theory/integral/lebesgue.lean
feat(measure_theory/integral/lebesgue): integral over finite and countable sets (#14447)
Added measure_theory.lintegral_singletonView on Github →