hasDerivAt_arccos — Mathlib

English

For x with x ≠ −1 and x ≠ 1, arccos has a derivative given by −1/√(1 − x^2).

Русский

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

LaTeX

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

Lean4

theorem hasDerivAt_arccos {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) : HasDerivAt arccos (-(1 / √(1 - x ^ 2))) x :=
  (hasDerivAt_arcsin h₁ h₂).const_sub (π / 2)

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