sin_lt — Mathlib

English

If 0 < x < π/2, then (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

/-- For 0 < x, we have sin x < x. -/
theorem sin_lt (h : 0 < x) : sin x < x := by
  rcases lt_or_ge 1 x with h' | h'
  · exact (sin_le_one x).trans_lt h'
  have hx : |x| = x := abs_of_nonneg h.le
  have := le_of_abs_le (sin_bound <| show |x| ≤ 1 by rwa [hx])
  rw [sub_le_iff_le_add', hx] at this
  apply this.trans_lt
  rw [sub_add, sub_lt_self_iff, sub_pos, div_eq_mul_inv (x ^ 3)]
  refine mul_lt_mul' ?_ (by norm_num) (by norm_num) (pow_pos h 3)
  apply pow_le_pow_of_le_one h.le h'
  simp

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