hasStrictDerivAt — Mathlib

English

An affine map f has a strictly differentiable derivative equal to its linear part at every point: HasStrictDerivAt f (f.linear 1) x.

Русский

Аффинное отображение f имеет строго дифференцируемую производную, равную его линейной части, в любой точке: HasStrictDerivAt f (f.linear 1) x.

LaTeX

$$$$ HasStrictDerivAt f (f.linear 1) x. $$$$

Lean4

theorem hasStrictDerivAt : HasStrictDerivAt f (f.linear 1) x :=
  by
  rw [f.decomp]
  exact f.linear.hasStrictDerivAt.add_const (f 0)

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