eqOn_dslope_slope

Mathlib.Analysis.Calculus.DSlope

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

English

dslope and slope agree off the point a, i.e., on the complement of {a}.

Русский

dslope и slope совпадают за пределами точки a, на множестве {a}ᶜ.

LaTeX

$$$ EqOn (dslope f a) (slope f a) { a }^c $$$

Lean4

theorem eqOn_dslope_slope (f : 𝕜 → E) (a : 𝕜) : EqOn (dslope f a) (slope f a) { a }ᶜ := fun _ => dslope_of_ne f

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

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

Разделы

Аффилиация

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