contDiffOn_arcsin

Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

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

← MathLib Explorer

English

Arcsin is ContDiffOn of any order n on the domain ℝ \\ {−1, 1}.

Русский

Arcsin является ContDiffOn любой степени n на области ℝ \\ {−1, 1}.

LaTeX

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

Lean4

theorem contDiffOn_arcsin {n : WithTop ℕ∞} : ContDiffOn ℝ n arcsin {-1, 1}ᶜ := fun _x hx =>
  (contDiffAt_arcsin (mt Or.inl hx) (mt Or.inr hx)).contDiffWithinAt

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

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

Разделы

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

Аффилиация

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