differentiableWithinAt_const

Mathlib.Analysis.Calculus.FDeriv.Const

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

← MathLib Explorer

English

The zero map is differentiable within s at x.

Русский

Нулевое отображение дифференцируемо внутри s в точке x.

LaTeX

$$DifferentiableWithinAt 𝕜 (0 : E → F) s x$$

Lean4

@[fun_prop]
theorem differentiableWithinAt_const (c : F) : DifferentiableWithinAt 𝕜 (fun _ => c) s x :=
  DifferentiableAt.differentiableWithinAt (differentiableAt_const _)

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

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

Разделы

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

Аффилиация

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