Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-01 15:09 df057e32

View on Github →

feat(measure_theory/integral/lebesgue): integral over finite and countable sets (#14447)

Estimated changes

Modified src/measure_theory/integral/lebesgue.lean

added theorem measure_theory.lintegral_countable

modified theorem measure_theory.lintegral_encodable

added theorem measure_theory.lintegral_finset

added theorem measure_theory.lintegral_fintype

added theorem measure_theory.lintegral_insert

added theorem measure_theory.lintegral_singleton'

added theorem measure_theory.lintegral_singleton

added theorem measure_theory.lintegral_unique