hasFDerivWithinAt_singleton — Mathlib

English

For any f and x, the derivative within the singleton {x} is the zero linear map.

Русский

Для любой функции f и точки x производная внутри множества {x} равна нулевой линейной карте.

LaTeX

$$$HasFDerivWithinAt f 0 \{x\} x$$$

Lean4

@[fun_prop]
theorem hasFDerivWithinAt_singleton (f : E → F) (x : E) : HasFDerivWithinAt f (0 : E →L[𝕜] F) { x } x := by
  simp only [HasFDerivWithinAt, nhdsWithin_singleton, hasFDerivAtFilter_iff_isLittleO, isLittleO_pure,
    ContinuousLinearMap.zero_apply, sub_self]

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