mfderivWithin_zero_of_not_mdifferentiableWithinAt

Mathlib.Geometry.Manifold.MFDeriv.Basic

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

← MathLib Explorer

English

If not mdifferentiableWithinAt, then mfderivWithin equals zero.

Русский

Если не mdifferentiableWithinAt, то mfderivWithin равно нулю.

LaTeX

$$Not (MDifferentiableWithinAt I I' f s x) → mfderivWithin I I' f s x = 0$$

Lean4

theorem mfderivWithin_zero_of_not_mdifferentiableWithinAt (h : ¬MDifferentiableWithinAt I I' f s x) :
    mfderivWithin I I' f s x = 0 := by simp only [mfderivWithin, h, if_neg, not_false_iff]

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

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

Разделы

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

Аффилиация

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