fderivWithin — Mathlib

English

If f is a bounded linear map, then its Fréchet derivative within any s equals the same linear map, provided a differentiability hypothesis with a unique differentiability point holds.

Русский

Если f – ограниченное линейное отображение, то его производная внутри s равна той же линейной карте при условии уникальности точки дифференцирования.

LaTeX

$$$$ fderivWithin 𝕜 f s x = h.toContinuousLinearMap, \\; \\text{for all } x, s. $$$$

Lean4

theorem fderivWithin (h : IsBoundedLinearMap 𝕜 f) (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 f s x = h.toContinuousLinearMap :=
  by
  rw [DifferentiableAt.fderivWithin h.differentiableAt hxs]
  exact h.fderiv

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