hasDerivAtFilter_natCast — Mathlib

English

For any natural number n, the map n → F has derivative 0 with respect to x: HasDerivAtFilter (n : 𝕜 → F) 0 x L.

Русский

Для любого натурального числа n отображение n ↦ F имеет производную 0 в точке x: HasDerivAtFilter (n : 𝕜 → F) 0 x L.

LaTeX

$$$\frac{d}{dx} (n) = 0$$$

Lean4

theorem hasDerivAtFilter_natCast [NatCast F] (n : ℕ) : HasDerivAtFilter (n : 𝕜 → F) 0 x L :=
  hasDerivAtFilter_const _ _ _

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