Limit_of_Absolute_Value
Provedabsolute-valueanalysislimitsproofwiki
|x - xi| -> 0 as x -> xi.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Limit_of_Absolute_Value (ξ : ℝ) : Filter.Tendsto (fun x => |x - ξ|) (nhds ξ) (nhds 0) := by sorry
Source