hasDerivAt_ofNat — Mathlib

English

Let F be a normed space over 𝕜 and let n be a natural number. The function t ↦ ofNat(n) is constant, hence its derivative at every x is 0.

Русский

Пусть F — нормированное пространство над 𝕜 и пусть n — натуральное число. Функция t ↦ ofNat(n) константна, следовательно, её производная в любой точке равна нулю.

LaTeX

$$$\\forall x \\in \\mathbb{k},\\ HasDerivAt((\\mathrm{ofNat}(n) : \\mathbb{k} \\to F),\\ 0,\\, x).$$$

Lean4

theorem hasDerivAt_ofNat (n : ℕ) [OfNat F n] : HasDerivAt (ofNat(n) : 𝕜 → F) 0 x :=
  hasDerivAt_const _ _

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