tsum_toNNReal_eq — Mathlib

English

Under non-infinity assumptions, the NNReal-valued tsum equals the tsum of the toNNReal values.

Русский

При условии, что значения не достигают бесконечности, сумма NNReal равна сумме преобразованных значений.

LaTeX

$$$\\\\left(\\\\forall a, f(a) \\\\neq \\\\infty\\\\right) \\\\Rightarrow (\\\\sum' a, f(a)).toNNReal = \\\\sum' a, (f(a)).toNNReal$$$

Lean4

theorem tsum_toNNReal_eq {f : α → ℝ≥0∞} (hf : ∀ a, f a ≠ ∞) : (∑' a, f a).toNNReal = ∑' a, (f a).toNNReal :=
  (congr_arg ENNReal.toNNReal (tsum_congr fun x => (coe_toNNReal (hf x)).symm)).trans NNReal.tsum_eq_toNNReal_tsum.symm

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