differentiableAt_inv_iff — Mathlib

English

Differentiability of the reciprocal function at x is equivalent to x ≠ 0.

Русский

Дифференцируемость функции r ↦ 1/r в точке r эквивалентна тому, что r ≠ 0.

LaTeX

$$$$DifferentiableAt\ 𝕜\ (\lambda x, x^{-1})\ x \iff x \neq 0.$$$$

Lean4

theorem differentiableAt_inv_iff : DifferentiableAt 𝕜 (fun x => x⁻¹) x ↔ x ≠ 0 :=
  ⟨fun H => NormedField.continuousAt_inv.1 H.continuousAt, fun H => (hasDerivAt_inv H).differentiableAt⟩

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