sin_lt_sin_of_lt_of_le_pi_div_two

English

Let x ≤ y with −π/2 ≤ x and y ≤ π/2 and x < y; then sin x < sin y.

Русский

Пусть x ≤ y, при этом −π/2 ≤ x и y ≤ π/2 и x < y; тогда sin x < sin y.

LaTeX

$$$$-\frac{\pi}{2} \le x \le \frac{\pi}{2},\; -\frac{\pi}{2} \le y \le \frac{\pi}{2},\; x < y \Rightarrow \sin x < \sin y$$$$

Lean4

theorem sin_lt_sin_of_lt_of_le_pi_div_two {x y : ℝ} (hx₁ : -(π / 2) ≤ x) (hy₂ : y ≤ π / 2) (hxy : x < y) :
    sin x < sin y := by
  rw [← sub_pos, sin_sub_sin]
  have : 0 < sin ((y - x) / 2) := by apply sin_pos_of_pos_of_lt_pi <;> linarith
  have : 0 < cos ((y + x) / 2) := by refine cos_pos_of_mem_Ioo ⟨?_, ?_⟩ <;> linarith
  positivity

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