deriv — Mathlib

English

If (nhds x).EventuallyEq f1 f, then Eq (derivWithin f1 s x) (derivWithin f s x).

Русский

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

LaTeX

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

Lean4

theorem deriv {f g : 𝕜 → F} {s : Set 𝕜} (hfg : s.EqOn f g) (hs : IsOpen s) : s.EqOn (deriv f) (deriv g) :=
  by
  intro x hx
  rw [← derivWithin_of_isOpen hs hx, ← derivWithin_of_isOpen hs hx]
  exact derivWithin_congr hfg (hfg hx)

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