Commit 2020-09-20 20:05 884e90be

feat(measure_theory): Borel-Cantelli (#4166)

lemma measure_limsup_eq_zero {s : ℕ → set α} (hs : ∀ i, is_measurable (s i))
  (hs' : (∑' i, μ (s i)) ≠ ⊤) : μ (limsup at_top s) = 0

There is a converse statement that is also called Borel-Cantelli, but we can't state it yet, because we don't know what independent events are.