by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
proofwikiseries
Let k=0∑∞ak be a convergent series in R. Then x→1−lim\parenk=0∑∞akxk=k=0∑∞ak where x→1−lim denotes the limit from the left.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Abels_Theorem (a : ℕ → ℝ) (s : ℝ) (ha : HasSum a s) : Filter.Tendsto (fun x : ℝ => ∑' n, a n * x ^ n) (nhdsWithin 1 (Set.Iio 1)) (nhds s) := by sorry