hasStrictDerivAt — Mathlib

English

For a linear map e: 𝕜 →ₗ[𝕜] F, HasStrictDerivAt e (e 1) x holds at every x; the derivative is the constant e(1).

Русский

Для линейного отображения e: 𝕜 →ₗ[𝕜] F выполняется HasStrictDerivAt e (e 1) в любой точке; производная постоянна и равна e(1).

LaTeX

$$$\\text{HasStrictDerivAt} \\big(\\lambda x, e x\\big) \\,(e(1))\\,x$$$

Lean4

protected theorem hasStrictDerivAt : HasStrictDerivAt e (e 1) x :=
  e.toContinuousLinearMap₁.hasStrictDerivAt

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