hasStrictDerivAt_lineMap — Mathlib

English

The lineMap between a and b has strict derivative b − a at any x; i.e., HasStrictDerivAt(lineMap a b) (b - a) x.

Русский

Линейная карта по точкам a и b имеет строгую производную b−a в любой точке x.

LaTeX

$$$\\text{HasStrictDerivAt}_{𝕜}^{\\text{lineMap}}(\\text{lineMap }a\\,b)\\ (b-a)\\ x.$$$

Lean4

theorem hasStrictDerivAt_lineMap : HasStrictDerivAt (lineMap a b) (b - a) x := by
  simpa using (lineMap a b : 𝕜 →ᵃ[𝕜] E).hasStrictDerivAt

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