deriv — Mathlib

English

For any affine map f: 𝕜 →ᵃ[𝕜] E and any x, the derivative satisfies deriv f x = f.linear 1; in particular, the derivative is constant along the domain.

Русский

Для любого аффинного отображения f: 𝕜 →ᵃ[𝕜] E и любой точки x производная выполняется как deriv f x = f.linear 1; производная константна по области определения.

LaTeX

$$$\\mathrm{deriv}(f,x) = f_{\\mathrm{linear}}(1).$$$

Lean4

@[simp]
protected theorem deriv : deriv f x = f.linear 1 :=
  f.hasDerivAt.deriv

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