fderivWithin_id' — Mathlib

English

Variant stating fderivWithin for the identity function with the fun x => x form, under UniqueDiffWithinAt.

Русский

Вариант для fderivWithin от идентичности в форме fun x => x при условии UniqueDiffWithinAt.

LaTeX

$$$\mathrm{fderivWithin}_{\mathbb{K}}(\mathrm{fun}\;x\;:\;E\to E\;\mapsto x, s, x) = \mathrm{Id}_{\mathbb{K}} E$$$

Lean4

theorem fderivWithin_id' (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (fun x : E => x) s x = ContinuousLinearMap.id 𝕜 E :=
  fderivWithin_id hxs

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