congr_of_eventuallyEq_of_mem — Mathlib

English

If h is ContMDiffWithinAt I I' n f s x, and f1 equals f eventually along nhdsWithin s at x, and hx: f1 x = f x with x ∈ s, then ContMDiffWithinAt I I' n f1 s x.

Русский

Если h: ContMDiffWithinAt I I' n f s x, и f1 совпадает c f вплоть до nhdsWithin s в x, и x принадлежит s, тогда ContMDiffWithinAt I I' n f1 s x.

LaTeX

$$$h: ContMDiffWithinAt I I' n f s x \land (nhdsWithin x s).EventuallyEq f_1 f \land f_1 x = f x \Rightarrow ContMDiffWithinAt I I' n f_1 s x.$$$

Lean4

theorem congr_of_eventuallyEq_of_mem (h : ContMDiffWithinAt I I' n f s x) (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : x ∈ s) :
    ContMDiffWithinAt I I' n f₁ s x :=
  (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr_of_eventuallyEq_of_mem h h₁ hx

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