hasDerivAtFilter — Mathlib

English

An affine map f has HasDerivAtFilter with derivative equal to its linear part at any x and in any filter L: HasDerivAtFilter f (f.linear 1) x L.

Русский

У аффинного отображения f в любой точке x и в любом фильтре L выполняется HasDerivAtFilter f (f.linear 1) x L.

LaTeX

$$$$ HasDerivAtFilter f (f.linear 1) x L. $$$$

Lean4

theorem hasDerivAtFilter : HasDerivAtFilter f (f.linear 1) x L :=
  by
  rw [f.decomp]
  exact f.linear.hasDerivAtFilter.add_const (f 0)

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