Lean-Workbook Plus 33968: Trigonometric inequality

For each real $a$ and every $\varepsilon>0$, there is $\delta>0$ such that $|x-a|<\delta$ implies $|\sin x-\sin a|<\varepsilon$.

Source: Lean-Workbook row lean_workbook_plus_33968 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.