hasStrictFDerivAt — Mathlib

English

If a function is analytic at a point x, then it has a strict Fréchet derivative at x with derivative fderiv f x.

Русский

Если функция аналитична в точке x, то у неё есть строгая Фреше-разложение в точке x, дифференциалом является fderiv f x.

LaTeX

$$$\\text{AnalyticAt } f\\ x \\Rightarrow \\text{HasStrictFDerivAt } f (fderiv\\, f\\ x)\\ x$$$

Lean4

theorem hasStrictFDerivAt (h : AnalyticAt 𝕜 f x) : HasStrictFDerivAt f (fderiv 𝕜 f x) x :=
  by
  rcases h with ⟨p, hp⟩
  rw [hp.fderiv_eq]
  exact hp.hasStrictFDerivAt

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