hasFDerivWithinAt_id — Mathlib

English

Let f be the identity map on a normed space E. Then the Fréchet derivative of f at any x (within any subset s) is the identity linear map on E.

Русский

Пусть f — тождественное отображение на нормированном пространстве E. Тогда фредхетова производная f в любой точке x (на любом подмножестве s) равна тождественному линейному отображению на E.

LaTeX

$$$\operatorname{HasFDerivWithinAt}(\mathrm{id}_E, \mathrm{Id}_E, s, x)$$$

Lean4

@[fun_prop]
theorem hasFDerivWithinAt_id (x : E) (s : Set E) : HasFDerivWithinAt id (.id 𝕜 E) s x :=
  hasFDerivAtFilter_id _ _

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