deriv_arcsin — Mathlib

English

The derivative of arcsin is given by deriv arcsin x = 1/√(1 − x^2) for x ≠ −1, 1; with the derivative defined as 0 at the nondifferentiable points.

Русский

Производная arcsin равна 1/√(1 − x^2) для x ≠ −1, 1; в точках, где производная не существует, производная по определению равна 0.

LaTeX

$$$\\operatorname{deriv}(\\arcsin)(x) = \\begin{cases} \\dfrac{1}{\\sqrt{1 - x^2}}, & x \\neq -1,1, \\\\ 0, & x = \\pm 1. \\end{cases}$$$

Lean4

@[simp]
theorem deriv_arcsin : deriv arcsin = fun x => 1 / √(1 - x ^ 2) :=
  by
  funext x
  by_cases h : x ≠ -1 ∧ x ≠ 1
  · exact (hasDerivAt_arcsin h.1 h.2).deriv
  · rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_arcsin.1 h)]
    simp only [not_and_or, Ne, Classical.not_not] at h
    rcases h with (rfl | rfl) <;> simp

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