hasDerivAt_arcsin — Mathlib

English

Let x ∈ ℝ with x ≠ -1 and x ≠ 1. Then arcsin is differentiable at x with derivative 1/√(1 − x^2).

Русский

Пусть x ∈ ℝ и x ≠ −1, x ≠ 1. arcsin дифференцируема в точке x и её производная равна 1/√(1 − x^2).

LaTeX

$$$\\forall x \\in \\mathbb{R},\\; x \\neq -1 \\land x \\neq 1 \\Rightarrow HasDerivAt(\\arcsin, \\tfrac{1}{\\sqrt{1 - x^2}}, x).$$$

Lean4

theorem hasDerivAt_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) : HasDerivAt arcsin (1 / √(1 - x ^ 2)) x :=
  (hasStrictDerivAt_arcsin h₁ h₂).hasDerivAt

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