hasFDerivAt — Mathlib

English

For a bounded linear map f, HasFDerivWithinAt is equivalent to HasFDerivAt; i.e., the within-derivative equals the global derivative.

Русский

Для ограниченного линейного отображения f производная внутри совпадает с глобальной производной; HasFDerivWithinAt ⇔ HasFDerivAt.

LaTeX

$$$$ HasFDerivWithinAt f h.toContinuousLinearMap s x \\Longrightarrow HasFDerivAt f h.toContinuousLinearMap x. $$$$

Lean4

@[fun_prop]
theorem hasFDerivAt (h : IsBoundedLinearMap 𝕜 f) : HasFDerivAt f h.toContinuousLinearMap x :=
  h.hasFDerivAtFilter

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