hasDerivWithinAt — Mathlib

English

The derivative of the underlying function of an affine map is its linear part: HasDerivAt ((AffineMap.instFunLike 𝕜 𝕜 E).coe f) (f.linear 1) x.

Русский

Производная базовой функции аффинного отображения равна его линейной части.

LaTeX

$$$$ HasDerivAt ((AffineMap.instFunLike 𝕜 𝕜 E).coe f) (f.linear 1) x. $$$$

Lean4

theorem hasDerivWithinAt : HasDerivWithinAt f (f.linear 1) s x :=
  f.hasDerivAtFilter

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