differentiable — Mathlib

English

Let f be a bounded linear map between normed spaces. Then f is Fréchet differentiable at every point, and its derivative at any point is f itself.

Русский

Пусть f — ограниченная линейная отображение между нормированными пространствами. Тогда f дифференцируема по Фрете во всех точках, и производная в любой точке совпадает с f.

LaTeX

$$$$\text{If } f: E \to F \text{ is a bounded linear map, then } f \text{ is Fréchet differentiable at every } x \in E \text{ with } Df(x)=f. $$$$

Lean4

@[fun_prop]
theorem differentiable (h : IsBoundedLinearMap 𝕜 f) : Differentiable 𝕜 f := fun _ => h.differentiableAt

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