cos_lt_cos_of_nonneg_of_le_pi — Mathlib

English

Let 0 ≤ x ≤ y ≤ π. Then cos y ≤ cos x, with strict inequality when x < y.

Русский

Пусть 0 ≤ x ≤ y ≤ π. Тогда cos y ≤ cos x, причём при x < y выполняется строгое неравенство.

LaTeX

$$$0 \le x \le y \le \\pi \\Rightarrow \\cos y \\le \\cos x.$$$

Lean4

theorem cos_lt_cos_of_nonneg_of_le_pi {x y : ℝ} (hx₁ : 0 ≤ x) (hy₂ : y ≤ π) (hxy : x < y) : cos y < cos x :=
  by
  rw [← sin_pi_div_two_sub, ← sin_pi_div_two_sub]
  apply sin_lt_sin_of_lt_of_le_pi_div_two <;> linarith

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