hasFDerivWithinAt — Mathlib

English

If f is a bounded linear map, it has a Fréchet derivative within any set with the derivative given by the corresponding continuous linear map, uniformly in x.

Русский

Если f – ограниченное линейное отображение, то во внутренности любого множества производная существует и равна соответствующей непрерывной линейной карте, независимо от x.

LaTeX

$$$$ HasFDerivWithinAt f h.toContinuousLinearMap s x. $$$$

Lean4

@[fun_prop]
theorem hasFDerivWithinAt (h : IsBoundedLinearMap 𝕜 f) : HasFDerivWithinAt f h.toContinuousLinearMap s x :=
  h.hasFDerivAtFilter

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