derivWithin_eq_of_nhds — Mathlib

English

If hs: f1 =ᶠ[𝓝[s] x] f and hx: x ∈ s, then derivWithin f1 s x = derivWithin f s x.

Русский

Если hs: f1 ≈ f на nhdsWithin x s и hx: x ∈ s, то производные внутри совпадают.

LaTeX

$$$(f_1 =ᶠ[𝓝[s] x] f) \\rightarrow x \\in s \\rightarrow derivWithin f_1 s x = derivWithin f s x$$$

Lean4

theorem derivWithin_eq_of_nhds (hs : f₁ =ᶠ[𝓝 x] f) : derivWithin f₁ s x = derivWithin f s x :=
  (hs.filter_mono nhdsWithin_le_nhds).derivWithin_eq hs.self_of_nhds

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