Limit_of_Cosine_X_Minus_1_over_X
Provedcosine-functiondifferential-calculuslimitsproofwiki
The limit as x approaches 0 of (cos x - 1)/x equals 0.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Formal statement
theorem Limit_of_Cosine_X_Minus_1_over_X : Filter.Tendsto (fun x : ℝ => (Real.cos x - 1) / x) (nhdsWithin 0 {0}ᶜ) (nhds 0) := by sorrySource