differentiableWithinAt_arcsin_Iic

English

For every real x with x ≠ 1, arccos is differentiable within Iic x at x with derivative −1/√(1 − x^2).

Русский

Для каждого x ∈ ℝ при x ≠ 1 arccos дифференцируема внутри Iic x в точке x, производная равна −1/√(1 − x^2).

LaTeX

$$$\\text{DifferentiableWithinAt}(\\arccos, \\mathrm{Iic}\\;x, x) \\iff x \\neq 1.$$$

Lean4

theorem differentiableWithinAt_arcsin_Iic {x : ℝ} : DifferentiableWithinAt ℝ arcsin (Iic x) x ↔ x ≠ 1 :=
  by
  refine ⟨fun h => ?_, fun h => (hasDerivWithinAt_arcsin_Iic h).differentiableWithinAt⟩
  rw [← neg_neg x, ← image_neg_Ici] at h
  have := (h.comp (-x) differentiableWithinAt_id.fun_neg (mapsTo_image _ _)).fun_neg
  simpa [(· ∘ ·), differentiableWithinAt_arcsin_Ici] using this

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