mdifferentiablefWithinAt_iff — Mathlib

English

MDifferentiableWithinAt I I' f s x holds iff for f1 with f1 = f eventually near x, f1 is MDifferentiableWithinAt f s x.

Русский

MDifferentiableWithinAt I I' f s x эквивалентно тому, что для пары f и f1, где f1 стремится к f ближе к x, выполняется MDifferentiableWithinAt f1 s x.

LaTeX

$$$(\text{MDifferentiableWithinAt } I I' f s x) \iff (MDifferentiableWithinAt I I' f_1 s x)$ при $f_1 =^\{nhdsWithin x s\} f$$$

Lean4

theorem mdifferentiablefWithinAt_iff (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
    MDifferentiableWithinAt I I' f₁ s x ↔ MDifferentiableWithinAt I I' f s x :=
  differentiableWithinAt_localInvariantProp.liftPropWithinAt_congr_iff_of_eventuallyEq h₁ hx

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