ennreal_tsum' — Mathlib

English

A strengthened form of summation measurability: tsum' over i is measurable under suitable conditions.

Русский

Усиленная форма измеримости суммирования tsum'.

LaTeX

$$$\text{ennreal_tsum}'(h)$$$

Lean4

@[measurability, fun_prop]
theorem ennreal_tsum' {ι} [Countable ι] {f : ι → α → ℝ≥0∞} (h : ∀ i, Measurable (f i)) : Measurable (∑' i, f i) :=
  by
  convert Measurable.ennreal_tsum h with x
  exact tsum_apply (Pi.summable.2 fun _ => ENNReal.summable)

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