lean_workbook_plus_33968

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove by epsilon-delta (Cauchy definition) that \n $\lim_{x->a} \sin x = \sin a$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_33968 (a : ℝ) : ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| < δ → |sin x - sin a| < ε   :=  by sorry

Source