Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-17 13:18 48dc2492

View on Github →

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.

Estimated changes