Convergent_Sequence_Minus_Limit
Provedconvergent-sequence-minus-limitlimits-of-sequencesproofwiki
If a sequence x_n converges to l, then |x_n - l| converges to 0.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Convergent_Sequence_Minus_Limit (x : ℕ → ℝ) (l : ℝ) (h : Filter.Tendsto x Filter.atTop (nhds l)) : Filter.Tendsto (fun n => |x n - l|) Filter.atTop (nhds 0) := by sorry
Source