differentiableWithinAt_arccos_Ici

English

For all 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 differentiableWithinAt_arccos_Ici {x : ℝ} : DifferentiableWithinAt ℝ arccos (Ici x) x ↔ x ≠ -1 :=
  (differentiableWithinAt_const_sub_iff _).trans differentiableWithinAt_arcsin_Ici

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