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