derivWithin_eq — Mathlib

English

If f1 ≈ f on nhdsWithin x s and f1 x = f x, then derivWithin f1 s x = derivWithin f s x.

Русский

Если f1 и f совпадают в окрестности nhdsWithin x s, а f1 x = f x, то производная внутри равна.

LaTeX

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

Lean4

theorem derivWithin_eq (hs : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : derivWithin f₁ s x = derivWithin f s x :=
  by
  unfold derivWithin
  rw [hs.fderivWithin_eq hx]

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