one_sub_mul_le_cos — Mathlib

English

If x ≠ 0, then 1 − x^2/2 < cos x.

Русский

Пусть x ∈ ℝ, x ≠ 0. Тогда 1 − x^2/2 < cos x.

LaTeX

$$$\forall x \in \mathbb{R}, x \ne 0 \Rightarrow 1 - \dfrac{x^2}{2} < \cos x$$$

Lean4

/-- Half of **Jordan's inequality** for `cos`. -/
theorem one_sub_mul_le_cos (hx₀ : 0 ≤ x) (hx : x ≤ π / 2) : 1 - 2 / π * x ≤ cos x := by
  simpa [sin_pi_div_two_sub, mul_sub, div_mul_div_comm, mul_comm π, pi_pos.ne'] using
    mul_le_sin (x := π / 2 - x) (by simpa) (by simpa)

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