isSymmSndFDerivWithinAt_of_omega — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- If a function is analytic within a set at a point, then its second derivative is symmetric. -/
theorem isSymmSndFDerivWithinAt_of_omega (hf : ContDiffWithinAt 𝕜 ω f s x) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
    IsSymmSndFDerivWithinAt 𝕜 f s x :=
  by
  rw [isSymmSndFDerivWithinAt_iff_iteratedFDerivWithin hs hx]
  exact hf.domDomCongr_iteratedFDerivWithin hs hx _

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