lineDeriv_eq — Mathlib

English

If the line derivative is defined via line deriv within a neighborhood and two functions agree there, then their line derivatives are equal.

Русский

Если линейная производная задана через производную вдоль линии в окрестности, и две функции совпадают там, то их линейные производные равны.

LaTeX

$$$(nhdsWithin x s).EventuallyEq f_{0} f_{1} \\Rightarrow \\mathrm{lineDerivWithin}_{\\mathbb{K}}(f_{0},s;x,v) = \\mathrm{lineDerivWithin}_{\\mathbb{K}}(f_{1},s;x,v)$$$

Lean4

theorem lineDeriv_eq (h : f₁ =ᶠ[𝓝 x] f) : lineDeriv 𝕜 f₁ x v = lineDeriv 𝕜 f x v := by
  rw [← lineDerivWithin_univ, ← lineDerivWithin_univ, h.lineDerivWithin_eq_nhds]

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