ae_finite_setOf_mem — Mathlib

English

If the sum of μ(s_i) is finite, then almost every x belongs to only finitely many s_i.

Русский

Если сумма μ(s_i) конечна, то μ-a.e. верно, что x принадлежит лишь конечному числу s_i.

LaTeX

$$$\\\\sum_i μ(s_i) \\\\neq \\\\infty \\\\Rightarrow \\\\text{ae } x,\\\\ (\\\\{i \\\\mid x \\\\in s_i\\\\}.Finite))$$$

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 a.e. all points belong to finitely sets of the family. -/
theorem ae_finite_setOf_mem {s : ι → Set α} (h : ∑' i, μ (s i) ≠ ∞) : ∀ᵐ x ∂μ, {i | x ∈ s i}.Finite :=
  by
  rw [ae_iff, ← measure_limsup_cofinite_eq_zero h]
  congr 1 with x
  simp [mem_limsup_iff_frequently_mem, Filter.Frequently]

Похожие утверждения