mdifferentiableAt — Mathlib

English

If f is ContMDiffAt at x, then f is differentiable at x in the manifold sense.

Русский

Если f гладко в точке x в смысле ContMDiffAt, то f дифференцируема в точке x на уровне многообразий.

LaTeX

$$$ContMDiffAt I I' n f x \Rightarrow MDifferentiableAt I I' f x$$$

Lean4

theorem mdifferentiableAt (hf : ContMDiffAt I I' n f x) (hn : 1 ≤ n) : MDifferentiableAt I I' f x :=
  mdifferentiableWithinAt_univ.1 <| ContMDiffWithinAt.mdifferentiableWithinAt hf hn

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