hasStrictDerivAt_arccos — Mathlib

English

For x with x ≠ −1 and x ≠ 1, arccos has a strict derivative equal to −1/√(1 − x^2).

Русский

Для x при x ≠ −1 и x ≠ 1 у arccos строгая производная равна −1/√(1 − x^2).

LaTeX

$$$\\text{HasStrictDerivAt}(\\arccos, -\\frac{1}{\\sqrt{1 - x^2}}, x) \\;\\text{for } x \\neq -1,1.$$$

Lean4

theorem hasStrictDerivAt_arccos {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) : HasStrictDerivAt arccos (-(1 / √(1 - x ^ 2))) x :=
  (hasStrictDerivAt_arcsin h₁ h₂).const_sub (π / 2)

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