hasDerivAtFilter_const — Mathlib

English

For any x and any filter L, the derivative of the constant function c is 0 along L: HasDerivAtFilter (fun _ => c) 0 x L.

Русский

Для любого x и любого фильтра L производная константы c по L равна 0: HasDerivAtFilter (функция, возвращающая c) 0 x L.

LaTeX

$$$\frac{d}{dx} c = 0$$$

Lean4

theorem hasDerivAtFilter_const : HasDerivAtFilter (fun _ => c) 0 x L :=
  (hasFDerivAtFilter_const c x L).hasDerivAtFilter

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