Boundedness_of_Sine_X_over_X

Proved

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

analysisboundsproofwikitrigonometry

|sin(x)/x| <= 1 for all nonzero real x.

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Formal statement

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

theorem Boundedness_of_Sine_X_over_X (x : ℝ) (hx : x ≠ 0) : |Real.sin x / x| ≤ 1 := by sorry

Source

https://proofwiki.org/wiki/Boundedness_of_Sine_X_over_X

View graph