arccos

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

URI: https://scilib.ai/kg/mathlib#ContinuousWithinAt.arccos

English

For all x ∈ ℝ, tan(arccos x) = sqrt(1 - x^2)/x.

Русский

Для любого x ∈ ℝ, тангенс арккос x равен sqrt(1 - x^2)/x.

LaTeX

$$\tan(\arccos x) = \frac{\sqrt{1 - x^2}}{x}$$

Lean4

protected nonrec theorem arccos (h : ContinuousWithinAt f s x) : ContinuousWithinAt (arccos <| f ·) s x :=
  h.arccos

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

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

Разделы

Аффилиация

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