HasFDerivAt — Mathlib

English

HasFDerivWithinAt f f' s x is defined as HasFDerivAtFilter f f' x (𝓝[s] x).

Русский

Характеризуется: производная внутри множества определяется через фильтр nhds внутри s.

LaTeX

$$$\text{HasFDerivWithinAt } f f' s x := \text{HasFDerivAtFilter } f f' x (\mathcal{N}[s] x)$$$

Lean4

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

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