hasDerivAt — Mathlib

English

An affine map has HasDerivWithinAt with derivative equal to its linear part, within any set s at x: HasDerivWithinAt f (f.linear 1) s x.

Русский

Аффинное отображение имеет HasDerivWithinAt с производной, равной линейной части, внутри любого множества s в точке x.

LaTeX

$$$$ HasDerivWithinAt f (f.linear 1) s x. $$$$

Lean4

theorem hasDerivAt : HasDerivAt f (f.linear 1) x :=
  f.hasDerivAtFilter

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