hasFDerivAtFilter_const — Mathlib

English

The derivative of the constant map is zero when considered with respect to a filter.

Русский

Производная константной карты равна нулю в контексте фильтра.

LaTeX

$$$HasFDerivAtFilter (\lambda _ : E, c) 0 x L$ for any c and L.$$

Lean4

theorem hasFDerivAtFilter_const (c : F) (x : E) (L : Filter E) : HasFDerivAtFilter (fun _ => c) (0 : E →L[𝕜] F) x L :=
  .of_isLittleOTVS <| (IsLittleOTVS.zero _ _).congr_left fun _ => by simp only [zero_apply, sub_self, Pi.zero_apply]

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