contDiffAt_arcsin — Mathlib

English

For every x ∈ ℝ with x ≠ −1 and x ≠ 1, arcsin is C^n (infinitely differentiable of all orders) at x for any order n.

Русский

Для каждого x ∈ ℝ с x ≠ −1 и x ≠ 1 arcsin гладок до любой конечно-непрерывной степени в точке x.

LaTeX

$$$\\forall x \\in \\mathbb{R},\\; x \\neq -1 \\land x \\neq 1 \\Rightarrow \\forall n \\in \\text{WithTop } \\mathbb{N}^\\infty,\\; \\text{ContDiffAt}(\\mathbb{R}, n, \\arcsin, x).$$$

Lean4

theorem contDiffAt_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) {n : WithTop ℕ∞} : ContDiffAt ℝ n arcsin x :=
  (deriv_arcsin_aux h₁ h₂).2.of_le le_top

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