sin_le_mul

Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

URI: https://scilib.ai/kg/mathlib#Real.sin_le_mul

← MathLib Explorer

English

For -(π/2) ≤ x ≤ 0, sin x ≤ (2/π) x.

Русский

Для -(π/2) ≤ x ≤ 0 выполняется sin x ≤ (2/π) x.

LaTeX

$$$$ -(\\frac{\\pi}{2}) \\le x \\le 0 \\Rightarrow \\sin x \\le \\frac{2}{\\pi} x. $$$$

Lean4

/-- Half of **Jordan's inequality** for negative values. -/
theorem sin_le_mul (hx : -(π / 2) ≤ x) (hx₀ : x ≤ 0) : sin x ≤ 2 / π * x := by
  simpa using mul_le_sin (neg_nonneg.2 hx₀) (neg_le.2 hx)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru