theorem first_borel_cantelli {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {A : ℕ → Set Ω} (hA : ∑' (n : ℕ), μ (A n) ≠ ⊤) : μ (Filter.limsup A Filter.atTop) = 0

First Borel–Cantelli lemma. If ∑ₙ μ(Aₙ) < ∞, then the set of points belonging to infinitely many of the Aₙ has measure zero, i.e. μ(limsup Aₙ) = 0.