tsum_measure_le_measure_univ — Mathlib

English

The sum (in the extended nonnegative reals) of measures of a family of null-measurable sets is bounded above by the measure of the whole space, provided pairwise AEDisjointness.

Русский

Сумма мер множества, образованная семейством нулево измеримых множеств, не превышает меру всего пространства при условии попарной а-диссостойности (AEDisjoint).

LaTeX

$$$ \sum' i, μ(s_i) ≤ μ(univ) $$$

Lean4

theorem tsum_measure_le_measure_univ {s : ι → Set α} (hs : ∀ i, NullMeasurableSet (s i) μ)
    (H : Pairwise (AEDisjoint μ on s)) : ∑' i, μ (s i) ≤ μ (univ : Set α) :=
  by
  rw [ENNReal.tsum_eq_iSup_sum]
  exact iSup_le fun s => sum_measure_le_measure_univ (fun i _hi => hs i) fun i _hi j _hj hij => H hij

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