English
If the sum of μ {x | p_i x} is finite, then the measure of the set of x for which p_i x holds frequently is zero.
Русский
Если сумма μ({x : p_i x}) конечна, то мера множества x, для которых p_i x выполняется часто, равна нулю.
LaTeX
$$$\\\\sum_i μ\\\\{x : p_i x\\\\} \\\\neq \\\\infty \\\\Rightarrow \\\\mu\\\\\\\\{x : \\\\exists^{\\\\_\\\\infty} i, p_i x\\\\} = 0$$$
Lean4
/-- A version of the **Borel-Cantelli lemma**: if `pᵢ` is a sequence of predicates such that
`∑' i, μ {x | pᵢ x}` is finite, then the measure of `x` such that `pᵢ x` holds frequently as `i → ∞`
(or equivalently, `pᵢ x` holds for infinitely many `i`) is equal to zero. -/
theorem measure_setOf_frequently_eq_zero {p : ℕ → α → Prop} (hp : ∑' i, μ {x | p i x} ≠ ∞) :
μ {x | ∃ᶠ n in atTop, p n x} = 0 := by
simpa only [limsup_eq_iInf_iSup_of_nat, frequently_atTop, ← bex_def, setOf_forall, setOf_exists] using
measure_limsup_atTop_eq_zero hp
