differentiableAt_arcsin — Mathlib

English

For all real x, DifferentiableWithinAt arccos (Ici x) x is equivalent to x ≠ −1.

Русский

Для всех x ∈ ℝ дифференцируемость arccos внутри Ici x эквивалентна x ≠ −1.

LaTeX

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

Lean4

theorem differentiableAt_arcsin {x : ℝ} : DifferentiableAt ℝ arcsin x ↔ x ≠ -1 ∧ x ≠ 1 :=
  ⟨fun h =>
    ⟨differentiableWithinAt_arcsin_Ici.1 h.differentiableWithinAt,
      differentiableWithinAt_arcsin_Iic.1 h.differentiableWithinAt⟩,
    fun h => (hasDerivAt_arcsin h.1 h.2).differentiableAt⟩

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