dslope — Mathlib

English

For any function f: 𝕜 → E, the dslope at (a, a) equals the ordinary derivative deriv f a.

Русский

Для любой f: 𝕜 → E, dslope f a a равна производной deriv f a.

LaTeX

$$$ dslope f a a = deriv f a $$$

Lean4

/-- `dslope f a b` is defined as `slope f a b = (b - a)⁻¹ • (f b - f a)` for `a ≠ b` and
`deriv f a` for `a = b`. -/
noncomputable def dslope (f : 𝕜 → E) (a : 𝕜) : 𝕜 → E :=
  update (slope f a) a (deriv f a)

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