fderivWithin_zero_of_not_differentiableWithinAt

Mathlib.Analysis.Calculus.FDeriv.Defs

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

← MathLib Explorer

English

For any f, fderivWithin 𝕜 f univ equals fderiv 𝕜 f.

Русский

Для всякой f, fderivWithin 𝕜 funiv равно fderiv 𝕜 f.

LaTeX

$$$fderivWithin 𝕜 f univ = fderiv 𝕜 f$$$

Lean4

theorem fderivWithin_zero_of_not_differentiableWithinAt (h : ¬DifferentiableWithinAt 𝕜 f s x) :
    fderivWithin 𝕜 f s x = 0 := by simp [fderivWithin, h]

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

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

Разделы

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

Аффилиация

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