mathlib3
f99d6386 - feat(measure_theory): integral over a family of pairwise a.e. disjoint sets (#10268)

Commit

4 years ago

feat(measure_theory): integral over a family of pairwise a.e. disjoint sets (#10268) Also golf a few proofs

Author

urkud

Parents