mathlib3
d0456d3b - feat(measure_theory/borel_space): add ae_measurable versions of finset.measurable_prod and measurable.ennreal_tsum (#6217)

Commit

5 years ago

feat(measure_theory/borel_space): add ae_measurable versions of finset.measurable_prod and measurable.ennreal_tsum (#6217) Also add an ae_measurable version of `ae_lt_top`.

Author

RemyDegenne

Parents

42bb0c4b

mathlib3 d0456d3b - feat(measure_theory/borel_space): add ae_measurable versions of finset.measurable_prod and measurable.ennreal_tsum (#6217)

mathlib3
d0456d3b - feat(measure_theory/borel_space): add ae_measurable versions of finset.measurable_prod and measurable.ennreal_tsum (#6217)