Lean-Workbook Plus 37352: Trigonometric inequality

For every $\varepsilon>0$, there is $\delta>0$ such that $x\ne0$ and $|x|<\delta$ imply $|x\sin(1/x)|<\varepsilon$.

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