hasSum_toReal — Mathlib

English

Simplicity version: under mild assumptions, Tendsto toReal is equivalent to Tendsto.

Русский

Простая версия: при слабых предпосылках Tendsto toReal эквивалентно Tendsto.

LaTeX

$$tendsto_toReal_iff (xt) (hf) (hx) : equivalence of Tendsto toReal and Tendsto$$

Lean4

theorem hasSum_toReal {f : α → ℝ≥0∞} (hsum : ∑' x, f x ≠ ∞) : HasSum (fun x => (f x).toReal) (∑' x, (f x).toReal) :=
  by
  lift f to α → ℝ≥0 using ENNReal.ne_top_of_tsum_ne_top hsum
  simp only [coe_toReal, ← NNReal.coe_tsum, NNReal.hasSum_coe]
  exact (tsum_coe_ne_top_iff_summable.1 hsum).hasSum

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