mathlib

e8758ae0 - feat(measure_theory/*): a few lemmas about `(is_)measurable` in `Π i, π i` (#4948)