mul_lt_sin — Mathlib

English

For 0 < x < π/2, 2/π · x < sin x.

Русский

Для 0 < x < π/2 верно 2/π · x < sin x.

LaTeX

$$$$ 0 < x < \\frac{\\pi}{2} \\Rightarrow \\frac{2}{\\pi} x < \\sin x. $$$$

Lean4

theorem mul_lt_sin {x : ℝ} (hx : 0 < x) (hx' : x < π / 2) : 2 / π * x < sin x :=
  by
  rw [← inv_div]
  simpa [-inv_div, mul_inv_cancel_left₀ pi_div_two_pos.ne'] using
    @lt_sin_mul ((π / 2)⁻¹ * x) (mul_pos (inv_pos.2 pi_div_two_pos) hx)
      (by rwa [← div_eq_inv_mul, div_lt_one pi_div_two_pos])

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