tendsto_nhds

Mathlib.Analysis.Calculus.Gradient.Basic

URI: https://scilib.ai/kg/mathlib#HasGradientAtFilter.tendsto_nhds

English

From a tendsto result along L ≤ 𝓝 x, a HasGradientAtFilter yields a convergent value f L → f(x).

Русский

Из сходимости вдоль фильтра следует сходимость функции к значениям в точке

LaTeX

$$tendsto_nhds (hL) (h) : Tendsto f L (𝓝 (f x))$$

Lean4

nonrec theorem tendsto_nhds (hL : L ≤ 𝓝 x) (h : HasGradientAtFilter f f' x L) : Tendsto f L (𝓝 (f x)) :=
  h.tendsto_nhds hL

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

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

Разделы

Аффилиация

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