congr_of_eventuallyEq — Mathlib

English

If HasGradientWithinAt f f' s x holds and f₁ equals f almost everywhere near x within s (nhdsWithin x s), then HasGradientWithinAt f₁ f' s x.

Русский

Если внутри множества s градиент существует, и f₁ эквивалентна f в окрестности x внутри s, то градиент сохраняется для f₁ на s.

LaTeX

$$HasGradientWithinAt f f' s x → (nhdsWithin x s).EventuallyEq f₁ f → Eq (f₁ x) (f x) → HasGradientWithinAt f₁ f' s x$$

Lean4

theorem congr_of_eventuallyEq (h : HasGradientWithinAt f f' s x) (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
    HasGradientWithinAt f₁ f' s x :=
  HasGradientAtFilter.congr_of_eventuallyEq h h₁ hx

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