HasFDerivWithinAt — Mathlib

English

The derivative within the entire space equals the ordinary derivative: fderivWithin 𝕜 f univ = fderiv 𝕜 f.

Русский

Производная внутри всей области совпадает с обычной производной.

LaTeX

$$$fderivWithin 𝕜 f univ = fderiv 𝕜 f$$$

Lean4

/-- A function `f` has the continuous linear map `f'` as derivative at `x` within a set `s` if
`f x' = f x + f' (x' - x) + o (x' - x)` when `x'` tends to `x` inside `s`. -/
@[fun_prop]
def HasFDerivWithinAt (f : E → F) (f' : E →L[𝕜] F) (s : Set E) (x : E) :=
  HasFDerivAtFilter f f' x (𝓝[s] x)

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