theorem second_Borel_Cantelli {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {A : ℕ → Set Ω} (hm : ∀ (n : ℕ), MeasurableSet (A n)) (hindep : ProbabilityTheory.iIndepSet A μ) (hsum : ∑' (n : ℕ), μ (A n) = ⊤) : μ (Filter.limsup A Filter.atTop) = 1

Second Borel–Cantelli lemma. If the events Aₙ are (mutually) independent and ∑ₙ μ(Aₙ) = ∞, then almost every point belongs to infinitely many of the Aₙ, i.e. μ(limsup Aₙ) = 1.