feat(measure_theory): Borel-Cantelli (#4166)
```lean
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.
