English
If s_i is a countable family with finite total sum, then μ(limsup s cofinite) = 0.
Русский
Если {s_i} счётное семейство и сумма μ(s_i) не бесконечна, то μ(limsup s по cof) = 0.
LaTeX
$$$\\\\sum_i μ(s_i) \\\\neq \\\\infty \\\\Rightarrow \\\\mu(\\\\limsup s \\\\text{cofinite}) = 0$$$
Lean4
/-- One direction of the **Borel-Cantelli lemma**
(sometimes called the "*first* Borel-Cantelli lemma"):
if `(s i)` is a sequence of sets such that `∑' i, μ (s i)` is finite,
then the limit superior of the `s i` along the `atTop` filter is a null set.
Note: for the *second* Borel-Cantelli lemma (applying to independent sets in a probability space),
see `ProbabilityTheory.measure_limsup_eq_one`. -/
theorem measure_limsup_atTop_eq_zero {s : ℕ → Set α} (hs : ∑' i, μ (s i) ≠ ∞) : μ (limsup s atTop) = 0 := by
rw [← Nat.cofinite_eq_atTop, measure_limsup_cofinite_eq_zero hs]
