hasStrictDerivAt_arcsin — Mathlib

English

Let x be a real number with x ≠ -1 and x ≠ 1. Then arcsin has a strict derivative at x with value 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 HasStrictDerivAt(\\arcsin, \\tfrac{1}{\\sqrt{1 - x^2}}, x).$$$

Lean4

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

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