lineDerivWithin_eq — Mathlib

English

If a function f changes by an equal amount in a neighborhood of x, then its line derivative is unchanged.

Русский

Если функция f меняется эквивалентно в окрестности x, то её линейная производная не меняется.

LaTeX

$$If f1 = f in nhds(x), then lineDerivative at x in direction v is unchanged: lineDerivWithin 𝕜 f1 s x v = lineDerivWithin 𝕜 f s x v$$

Lean4

theorem lineDerivWithin_eq (hs : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
    lineDerivWithin 𝕜 f₁ s x v = lineDerivWithin 𝕜 f s x v :=
  by
  apply derivWithin_eq ?_ (by simpa using hx)
  have A : Continuous (fun (t : 𝕜) ↦ x + t • v) := by fun_prop
  exact A.continuousWithinAt.preimage_mem_nhdsWithin'' hs (by simp)

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