differentiableAt_ofNat

Mathlib.Analysis.Calculus.FDeriv.Const

URI: https://scilib.ai/kg/mathlib#differentiableAt_ofNat

← MathLib Explorer

English

For any n, DifferentiableWithinAt 𝕜 (ofNat n) s x.

Русский

Для любого n дифференцируемость внутри множества s для отображения ofNat n.

LaTeX

$$DifferentiableWithinAt 𝕜 ((ofNat n) : E → F) s x$$

Lean4

@[simp low, fun_prop]
theorem differentiableAt_ofNat (n : ℕ) [OfNat F n] (x : E) : DifferentiableAt 𝕜 (ofNat(n) : E → F) x :=
  differentiableAt_const _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru