English
A symmetry condition for the second derivative within a set s at x, encoded by IsSymmSndFDerivWithinAt.
Русский
Условие симметрии второго производной внутри множества в точке x.
LaTeX
$$$\\text{IsSymmSndFDerivWithinAt}_{\\mathbb{K}}(f,s,x)$$$
Lean4
/-- Definition recording that a function has a symmetric second derivative within a set at
a point. This is automatic in most cases of interest (open sets over real or complex vector fields,
or general case for analytic functions), but we can express theorems of calculus using this
as a general assumption, and then specialize to these situations. -/
def IsSymmSndFDerivWithinAt (f : E → F) (s : Set E) (x : E) : Prop :=
∀ v w, fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x v w = fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x w v
