deriv_eq

Mathlib.Analysis.Calculus.Deriv.Basic

URI: https://scilib.ai/kg/mathlib#Filter.EventuallyEq.deriv_eq

English

If f1 ≈ f in nhds x, then derivWithin f1 s x = derivWithin f s x.

Русский

Если f1 эквивалентна f в nhds x, то их derivWithin совпадают.

LaTeX

$$$(nhds x).EventuallyEq f_1 f \\rightarrow derivWithin f_1 s x = derivWithin f s x$$$

Lean4

theorem deriv_eq (hL : f₁ =ᶠ[𝓝 x] f) : deriv f₁ x = deriv f x :=
  by
  unfold deriv
  rwa [Filter.EventuallyEq.fderiv_eq]

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

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

Разделы

Аффилиация

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