contDiffOn_arccos

Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

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

English

ContDiffOn Real n arccos on the domain ℝ \ {−1,1}.

Русский

ContDiffOn Real n arccos на области ℝ \ {−1,1}.

LaTeX

$$$\\text{ContDiffOn}(\\mathbb{R}, n, \\arccos, {(-1,1)^c}).$$$

Lean4

theorem contDiffOn_arccos {n : WithTop ℕ∞} : ContDiffOn ℝ n arccos {-1, 1}ᶜ :=
  contDiffOn_const.sub contDiffOn_arcsin

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

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

Разделы

Аффилиация

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