abs_sin_half

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

URI: https://scilib.ai/kg/mathlib#Real.abs_sin_half

English

|sin(x/2)| = sqrt((1 − cos x)/2).

Русский

|sin(x/2)| = sqrt((1 − cos x)/2).

LaTeX

$$$$\left|\sin\left(\frac{x}{2}\right)\right| = \sqrt{\frac{1 - \cos x}{2}}$$$$

Lean4

theorem abs_sin_half (x : ℝ) : |sin (x / 2)| = √((1 - cos x) / 2) := by
  rw [← sqrt_sq_eq_abs, sin_sq_eq_half_sub, two_mul, add_halves, sub_div]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru