mathlib

48dc2492 - feat(measure_theory/measure): +1 version of Borel-Cantelli, drop an assumption (#9678)

feat(measure_theory/measure): +1 version of Borel-Cantelli, drop an assumption (#9678) * In all versions of Borel-Cantelli lemma, do not require that the sets are measurable. * Add +1 version. * Golf proofs.