differentiableWithinAt_arccos_Iic

English

For all x ∈ ℝ, DifferentiableWithinAt arccos (Iic x) x is equivalent to x ≠ 1.

Русский

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

LaTeX

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

Lean4

theorem differentiableWithinAt_arccos_Iic {x : ℝ} : DifferentiableWithinAt ℝ arccos (Iic x) x ↔ x ≠ 1 :=
  (differentiableWithinAt_const_sub_iff _).trans differentiableWithinAt_arcsin_Iic

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