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