hasFDerivAt_zero_of_eventually_const

English

If a function f: E → F is eventually constant near x (i.e., there exists c ∈ F with f(y) = c for all y sufficiently close to x), then the Fréchet derivative of f at x is the zero linear map.

Русский

Если функция f: E → F становится константной около точки x (существует c ∈ F такая, что f(y) = c для всех y близких к x), то производная Фреше в точке x равна нулю как линейному отображению.

LaTeX

$$$\big( \exists c \in F,\ f =^{\mathcal{N}_x}\! (\lambda y. c) \big) \rightarrow \text{HasFDerivAt } f (0 : E \toL[\mathcal{K}] F) x$$$

Lean4

theorem hasFDerivAt_zero_of_eventually_const (c : F) (hf : f =ᶠ[𝓝 x] fun _ => c) : HasFDerivAt f (0 : E →L[𝕜] F) x :=
  (hasFDerivAt_const _ _).congr_of_eventuallyEq hf

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