fderivWithin_eq_of_nhds — Mathlib

English

If f1 and f are equal in a neighborhood of x (in the ambient topology), then their derivatives within s at x are equal (as linear maps).

Русский

Если функции f1 и f равны в соседстве точки x (в топологическом смысле), то их производные внутри s в точке x равны.

LaTeX

$$$\exists U \ni x: U \subseteq s \land f|_U = f_1|_U \Rightarrow fderivWithin 𝕜 f_1 s x = fderivWithin 𝕜 f s x.$$$

Lean4

theorem fderivWithin_eq_of_nhds (h : f₁ =ᶠ[𝓝 x] f) : fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x :=
  (h.filter_mono nhdsWithin_le_nhds).fderivWithin_eq h.self_of_nhds

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