lineDerivWithin_eq_nhds — Mathlib

English

If f0 and f1 are equal near x and agree at x, then the line derivative value at x along v is the same for f0 and f1.

Русский

Если f0 и f1 совпадают рядом с x и в x совпадают значения, то производная вдоль направления v одинакова.

LaTeX

$$$(nhds x).EventuallyEq f_{0} f_{1} \\land f_{0}(x)=f_{1}(x) \\Rightarrow \\mathrm{lineDeriv}_{\\mathbb{K}}(f_{0},x,v) = \\mathrm{lineDeriv}_{\\mathbb{K}}(f_{1},x,v)$$$

Lean4

theorem lineDerivWithin_eq_nhds (h : f₁ =ᶠ[𝓝 x] f) : lineDerivWithin 𝕜 f₁ s x v = lineDerivWithin 𝕜 f s x v :=
  (h.filter_mono nhdsWithin_le_nhds).lineDerivWithin_eq h.self_of_nhds

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