sin_pos_of_pos_of_lt_pi — Mathlib

English

For all x ∈ ℝ and integer n, sin(x + nπ) = (-1)^n sin x.

Русский

Для любого x ∈ ℝ и целого n верно sin(x + nπ) = (-1)^n sin x.

LaTeX

$$$\forall x \in \mathbb{R},\ \forall n \in \mathbb{Z},\ \sin\left(x + n\pi\right) = (-1)^n \sin x$$$

Lean4

theorem sin_pos_of_pos_of_lt_pi {x : ℝ} (h0x : 0 < x) (hxp : x < π) : 0 < sin x :=
  if hx2 : x ≤ 2 then sin_pos_of_pos_of_le_two h0x hx2
  else
    have : (2 : ℝ) + 2 = 4 := by norm_num
    have : π - x ≤ 2 := sub_le_iff_le_add.2 (le_trans pi_le_four (this ▸ add_le_add_left (le_of_not_ge hx2) _))
    sin_pi_sub x ▸ sin_pos_of_pos_of_le_two (sub_pos.2 hxp) this

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