dslope_eventuallyEq_slope_nhdsNE

Mathlib.Analysis.Calculus.DSlope

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

← MathLib Explorer

English

In the nhdsNE of a, dslope equals slope almost everywhere away from a.

Русский

В nhdsNE точки a dslope совпадает со slope почти всюду кроме a.

LaTeX

$$$ dslope f a =^{{\ nhdsNE}} slope f a $$$

Lean4

theorem dslope_eventuallyEq_slope_nhdsNE (f : 𝕜 → E) : dslope f a =ᶠ[𝓝[≠] a] slope f a :=
  (eqOn_dslope_slope f a).eventuallyEq_of_mem self_mem_nhdsWithin

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

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

Разделы

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

Аффилиация

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