English
If a monotone sequence of sets s_n has tail-sum condition not top, then μ(⋃ n s_n) = ⨆ n μ(s_n).
Русский
Если монотонная последовательность множеств s_n имеет условие хвостовой суммы, не дающее бесконечности, то μ(⋃ n s_n) = ⨆ n μ(s_n).
LaTeX
$$$\\\\mu\\\\left\\\\(\\\\\\\\bigcup_{n} s_n\\\\right\\\\) = \\\\sup_{n} μ(s_n)$$$
Lean4
/-- One direction of the **Borel-Cantelli lemma**
(sometimes called the "*first* Borel-Cantelli lemma"):
if `(s i)` is a countable family of sets such that `∑' i, μ (s i)` is finite,
then the limit superior of the `s i` along the cofinite 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_cofinite_eq_zero {s : ι → Set α} (hs : ∑' i, μ (s i) ≠ ∞) : μ (limsup s cofinite) = 0 :=
by
refine bot_unique <| ge_of_tendsto' (ENNReal.tendsto_tsum_compl_atTop_zero hs) fun t ↦ ?_
calc
μ (limsup s cofinite) ≤ μ (⋃ i : { i // i ∉ t }, s i) :=
by
gcongr
rw [hasBasis_cofinite.limsup_eq_iInf_iSup, iUnion_subtype]
exact iInter₂_subset _ t.finite_toSet
_ ≤ ∑' i : { i // i ∉ t }, μ (s i) := measure_iUnion_le _
