differentiableAt — Mathlib

English

If a function f is C^n at a point x with n ≥ 1, then f is differentiable at x.

Русский

Если функция f является C^n в точке x и n ≥ 1, то она дифференцируема в этой точке x.

LaTeX

$$$ContDiffAt\ 𝕜\ n\ f\ x\ ∧ 1 \le n\Rightarrow DifferentiableAt\ 𝕜\ f\ x$$$

Lean4

/-- If a function is `C^n` with `n ≥ 1` at a point, then it is differentiable there. -/
theorem differentiableAt (h : ContDiffAt 𝕜 n f x) (hn : 1 ≤ n) : DifferentiableAt 𝕜 f x := by
  simpa [hn, differentiableWithinAt_univ] using h.differentiableWithinAt

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