hasStrictFDerivAt — Mathlib

English

Let e be a continuous linear map E → F between normed spaces. Then the Fréchet derivative of the map e at every point x is e itself.

Русский

Пусть e — непрерывное линейное отображение E → F между нормированными пространствами. Производная Фреше от отображения e в любой точке x равна самому отображению e.

LaTeX

$$$\text{The Fréchet derivative of } e \text{ at } x \text{ is } e$, i.e. $D e(x) = e$.$$

Lean4

@[fun_prop]
protected theorem hasStrictFDerivAt {x : E} : HasStrictFDerivAt e e x :=
  .of_isLittleOTVS <| (IsLittleOTVS.zero _ _).congr_left fun x => by simp only [e.map_sub, sub_self, Pi.zero_apply]

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