hasDerivAtFilter — Mathlib

English

Let e: 𝕜 →ₗ[𝕜] F be a linear map. The derivative of the function x ↦ e x is constantly e(1); equivalently, the derivative at any x (in the sense of HasDerivAt) equals e(1).

Русский

Пусть e: 𝕜 →ₗ[𝕜] F — линейное отображение. Производная функции x ↦ e x постоянна и равна e(1); иначе говоря, во всех точках x производная равна e(1).

LaTeX

$$$\\exists ! \\,\, d: F,\\; d = e(1) \\quad\\text{and}\\quad \\text{HasDerivAt} (\\lambda x, e x) d \\;\\text{at every } x$$$

Lean4

protected theorem hasDerivAtFilter : HasDerivAtFilter e (e 1) x L :=
  e.toContinuousLinearMap₁.hasDerivAtFilter

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