measure_liminf_cofinite_eq_zero — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem measure_liminf_cofinite_eq_zero [Infinite ι] {s : ι → Set α} (h : ∑' i, μ (s i) ≠ ∞) :
    μ (liminf s cofinite) = 0 :=
  by
  rw [← le_zero_iff, ← measure_limsup_cofinite_eq_zero h]
  exact measure_mono liminf_le_limsup

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