sin_le_sin_of_le_of_le_pi_div_two

English

Let -(π/2) ≤ x ≤ y ≤ π/2. Then sin x ≤ sin y.

Русский

Пусть -(π/2) ≤ x ≤ y ≤ π/2. Тогда sin x ≤ sin y.

LaTeX

$$$-\\frac{\\pi}{2} \\le x \\le y \\le \\frac{\\pi}{2} \\Rightarrow \\sin x \\le \\sin y.$$$

Lean4

theorem sin_le_sin_of_le_of_le_pi_div_two {x y : ℝ} (hx₁ : -(π / 2) ≤ x) (hy₂ : y ≤ π / 2) (hxy : x ≤ y) :
    sin x ≤ sin y :=
  (strictMonoOn_sin.le_iff_le ⟨hx₁, hxy.trans hy₂⟩ ⟨hx₁.trans hxy, hy₂⟩).2 hxy

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