differentiableOn_arccos

Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

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

English

Arccos is differentiable on ℝ outside {−1,1}; i.e., differentiable on the complement of {−1,1}.

Русский

arccos дифференцируема на ℝ \ {−1,1}.

LaTeX

$$$\\text{DifferentiableOn}(\\arccos, \\mathbb{R} \\setminus \\{ -1, 1 \\}).$$$

Lean4

theorem differentiableOn_arccos : DifferentiableOn ℝ arccos {-1, 1}ᶜ :=
  differentiableOn_arcsin.const_sub _

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

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

Разделы

Аффилиация

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