differentiable — Mathlib

English

Let 𝕜 be a nontrivial normed field and V, W normed spaces over 𝕜. Then any continuous affine map f: V →ᴬ[𝕜] W is differentiable (Fréchet differentiable) everywhere.

Русский

Пусть 𝕜 — ненулевое нормированное поле, V и W — нормированные пространства над 𝕜. Любое непрерывное аффинное отображение f: V →ᴬ[𝕜] W дифференцируемо повсюду (дифференцируемо во Фреше).

LaTeX

$$$ \operatorname{Differentiable}_{\mathbb{k}}(f). $$$

Lean4

theorem differentiable (f : V →ᴬ[𝕜] W) : Differentiable 𝕜 f :=
  f.contDiff.differentiable le_rfl

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