differentiableAt_arccos

Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

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

← MathLib Explorer

English

DifferentiableAt arccos x is equivalent to x ≠ −1 and x ≠ 1.

Русский

Производимость arccos в точке x эквивалентна x ≠ −1 и x ≠ 1.

LaTeX

$$$\\text{DifferentiableAt}(\\arccos, x) \\iff x \\neq -1 \\land x \\neq 1.$$$

Lean4

theorem differentiableAt_arccos {x : ℝ} : DifferentiableAt ℝ arccos x ↔ x ≠ -1 ∧ x ≠ 1 :=
  (differentiableAt_const _).sub_iff_right.trans differentiableAt_arcsin

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

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

Разделы

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

Аффилиация

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