fderivWithin_eventually_congr_set

English

The derivative of the function y ↦ (c(y)) u at x is given by the action of the flipped derivative on u.

Русский

Производная функции y ↦ (c(y)) u в точке x равна действию развернутой производной на u.

LaTeX

$$$fderivWithin 𝕜 (y \\mapsto (c(y))u) s x = (fderivWithin 𝕜 c s x) \\;u.$$$

Lean4

theorem fderivWithin_eventually_congr_set (h : s =ᶠ[𝓝 x] t) : fderivWithin 𝕜 f s =ᶠ[𝓝 x] fderivWithin 𝕜 f t :=
  fderivWithin_eventually_congr_set' x <| h.filter_mono inf_le_left

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