fderivWithin_fderivWithin_eq_of_mem_nhds

English

If a function is analytic within a set at a point, then its second derivative is symmetric.

Русский

Если функция аналитична на множестве в точке, то её вторая производная симметрична.

LaTeX

$$$\\text{ContDiffWithinAt}_{\\mathbb{K}}(2,f,s,x) \\Rightarrow \\text{IsSymmSndFDerivWithinAt}_{\\mathbb{K}}(f,s,x)$$$

Lean4

theorem fderivWithin_fderivWithin_eq_of_mem_nhds {f : E → F} {x : E} {s : Set E} (h : s ∈ 𝓝 x) :
    fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x = fderiv 𝕜 (fderiv 𝕜 f) x :=
  by
  simp only [← fderivWithin_univ]
  apply fderivWithin_fderivWithin_eq_of_eventuallyEq
  simp [h]

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