hasDerivWithinAt_lineMap — Mathlib

English

The lineMap between a and b has derivative b − a within s at x; i.e., HasDerivWithinAt(lineMap a b) (b − a) s x.

Русский

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

LaTeX

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

Lean4

theorem hasDerivWithinAt_lineMap : HasDerivWithinAt (lineMap a b) (b - a) s x :=
  hasDerivAt_lineMap.hasDerivWithinAt

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