measure_liminf_atTop_eq_zero — Mathlib

English

If ι is infinite and the sum of μ(s_i) is finite, then μ(liminf s atTop) = 0.

Русский

Если ι бесконечен и сумма μ(s_i) конечна, то μ(liminf s при atTop) = 0.

LaTeX

$$$[Infinite \\\\ ι] \\\\Rightarrow μ\\\$\\\\liminf s \\\\text{ atTop}\\\$ = 0$$$

Lean4

theorem measure_liminf_atTop_eq_zero {s : ℕ → Set α} (h : (∑' i, μ (s i)) ≠ ∞) : μ (liminf s atTop) = 0 := by
  rw [← Nat.cofinite_eq_atTop, measure_liminf_cofinite_eq_zero h]
    -- TODO: the next 2 lemmas are true for any filter with countable intersections, not only `ae`.
    -- Need to specify `α := Set α` below because of diamond; see https://github.com/leanprover-community/mathlib4/pull/19041

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