nnreal_tsum — Mathlib

English

If each f_i is measurable to NNReal, then tsum of f_i is measurable.

Русский

Если каждая f_i измерима в NNReal, то tsum измеримо.

LaTeX

$$$\forall i, \text{Measurable}(f_i) \Rightarrow \text{Measurable}(\sum_i f_i)$$$

Lean4

@[measurability, fun_prop]
theorem nnreal_tsum {ι} [Countable ι] {f : ι → α → ℝ≥0} (h : ∀ i, Measurable (f i)) : Measurable fun x => ∑' i, f i x :=
  by
  simp_rw [NNReal.tsum_eq_toNNReal_tsum]
  exact (Measurable.ennreal_tsum fun i => (h i).coe_nnreal_ennreal).ennreal_toNNReal

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