toNNReal_apply_of_tsum_ne_top — Mathlib

English

If ∑' i, f(i) ≠ ∞, then for every x, (toNNReal (f(x))) = ENNReal.toNNReal (f(x)) and coincides with f(x) when reinterpreted as ENNReal.

Русский

Если сумма не бесконечна, то для каждого x имеет место равенство toNNReal f(x) = f(x) после соответствующего отображения.

LaTeX

$$$\Big(\sum' i, f(i) \neq \infty\Big) \rightarrow ((\mathrm{toNNReal} \circ f)(x) : \mathbb{R}_{\ge 0}) = f(x)$$$

Lean4

theorem toNNReal_apply_of_tsum_ne_top {α : Type*} {f : α → ℝ≥0∞} (hf : ∑' i, f i ≠ ∞) (x : α) :
    (((ENNReal.toNNReal ∘ f) x : ℝ≥0) : ℝ≥0∞) = f x :=
  coe_toNNReal <| ENNReal.ne_top_of_tsum_ne_top hf _

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