Sequence_of_Powers_of_Reciprocals_is_Null_Sequence
Provedlimits-of-sequencesnull-sequencesproofwiki
If |x| < 1, then the sequence x^n converges to 0.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Sequence_of_Powers_of_Reciprocals_is_Null_Sequence (x : ℝ) (hx : |x| < 1) : Filter.Tendsto (fun n : ℕ => x ^ n) Filter.atTop (nhds 0) := by sorry
Source