hasDerivAtFilter

Mathlib.Analysis.Calculus.Deriv.Basic

URI: https://scilib.ai/kg/mathlib#HasFDerivAtFilter.hasDerivAtFilter

English

Equivalence between HasFDerivWithinAt f f' s x and HasDerivWithinAt f (f' 1) s x.

Русский

Эквивалентность между HasFDerivWithinAt f f' s x и HasDerivWithinAt f (f' 1) s x.

LaTeX

$$$\\text{HasFDerivWithinAt}(f,f',s,x) \\iff \\text{HasDerivWithinAt}(f,(f'\\,1),s,x).$$$

Lean4

theorem hasDerivAtFilter {f' : 𝕜 →L[𝕜] F} : HasFDerivAtFilter f f' x L → HasDerivAtFilter f (f' 1) x L :=
  hasFDerivAtFilter_iff_hasDerivAtFilter.mp

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

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

Разделы

Аффилиация

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