mdifferentiableAt_iff — Mathlib

English

If f and f1 are eventually equal near x with respect to s, then mdifferentiablewithinAt f equals mdifferentiablewithinAt f1.

Русский

Если f и f1 равны по существу в окрестности x относительно s, то mdifferentiablewithinAt f совпадает с mdifferentiablewithinAt f1.

LaTeX

$$$\text{(nhdsWithin x s).EventuallyEq f_1 f} \Rightarrow MDifferentiableWithinAt I I' f_1 s x \Leftrightarrow MDifferentiableWithinAt I I' f s x$$$

Lean4

theorem mdifferentiableAt_iff (h₁ : f₁ =ᶠ[𝓝 x] f) : MDifferentiableAt I I' f₁ x ↔ MDifferentiableAt I I' f x :=
  differentiableWithinAt_localInvariantProp.liftPropAt_congr_iff_of_eventuallyEq h₁

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