ae_eventually_notMem — Mathlib

English

A variant of the above: if hp: sum of μ {x | p_i x} is finite, then μ {x | p_i x holds frequently} = 0.

Русский

Вариант выше: если сумма μ {x : p_i x} конечна, то мера множества x, для которых p_i x выполняется часто, равна нулю.

LaTeX

$$$\\\\sum_i μ\\\\{x : p_i x\\\\} \\\\neq \\\\infty \\\\Rightarrow \\\\mu\\\\{x : \\\\text{Frequently } (p_i x)\\\\} = 0$$$

Lean4

/-- A version of the **Borel-Cantelli lemma**: if `sᵢ` is a sequence of sets such that
`∑' i, μ sᵢ` is finite, then for almost all `x`, `x` does not belong to `sᵢ` for large `i`. -/
theorem ae_eventually_notMem {s : ℕ → Set α} (hs : (∑' i, μ (s i)) ≠ ∞) : ∀ᵐ x ∂μ, ∀ᶠ n in atTop, x ∉ s n :=
  measure_setOf_frequently_eq_zero hs

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