le_sin_mul

Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

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

← MathLib Explorer

English

If 0 ≤ x ≤ 1, then x ≤ sin((π/2) x).

Русский

Если 0 ≤ x ≤ 1, то x ≤ sin((π/2) x).

LaTeX

$$$$ 0 \\le x \\le 1 \\Rightarrow x \\le \\sin\\left(\\frac{\\pi}{2} x\\right). $$$$

Lean4

theorem le_sin_mul {x : ℝ} (hx : 0 ≤ x) (hx' : x ≤ 1) : x ≤ sin (π / 2 * x) := by
  simpa [mul_comm x] using
    strictConcaveOn_sin_Icc.concaveOn.2 ⟨le_rfl, pi_pos.le⟩ ⟨pi_div_two_pos.le, half_le_self pi_pos.le⟩
      (sub_nonneg.2 hx') hx

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

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

Разделы

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

Аффилиация

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