hasDerivWithinAt_arccos_Ici — Mathlib

English

For x ≠ −1, HasDerivWithinAt arccos (−1/√(1 − x^2)) on Ici x at x.

Русский

Для x ≠ −1 имеет место HasDerivWithinAt arccos (−1/√(1 − x^2)) на Ici x в точке x.

LaTeX

$$$\\text{HasDerivWithinAt}(\\arccos, -\\frac{1}{\\sqrt{1 - x^2}}, \\mathrm{Ici}\\;x, x).$$$

Lean4

theorem hasDerivWithinAt_arccos_Ici {x : ℝ} (h : x ≠ -1) : HasDerivWithinAt arccos (-(1 / √(1 - x ^ 2))) (Ici x) x :=
  (hasDerivWithinAt_arcsin_Ici h).const_sub _

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