cos_half

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

← MathLib Explorer

English

cos(π/2 − x) = sin x.

Русский

cos(π/2 − x) = sin x.

LaTeX

$$$$\cos\left(\frac{\pi}{2} - x\right) = \sin x$$$$

Lean4

theorem cos_half {x : ℝ} (hl : -π ≤ x) (hr : x ≤ π) : cos (x / 2) = √((1 + cos x) / 2) :=
  by
  have : 0 ≤ cos (x / 2) := cos_nonneg_of_mem_Icc <| by constructor <;> linarith
  rw [← sqrt_sq this, cos_sq, add_div, two_mul, add_halves]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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