cos_arccos

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

English

If -1 ≤ x ≤ 1, then cos(arccos x) = x.

Русский

Если -1 ≤ x ≤ 1, то cos(arccos x) = x.

LaTeX

$$\-1 \le x \le 1 \Rightarrow \cos(\arccos x) = x$$

Lean4

theorem cos_arccos {x : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) : cos (arccos x) = x := by
  rw [arccos, cos_pi_div_two_sub, sin_arcsin hx₁ hx₂]

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

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

Разделы

Аффилиация

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