congr_of_eventuallyEq — Mathlib

English

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

Русский

Если h = ContMDiffWithinAt I I' n f s x и f1 совпадает с f вплоть до предела nhdsWithin s в x, и x ∈ s, а также f1 x = f x, то f1 является ContMDiffWithinAt I I' n f s x.

LaTeX

$$$h: ContMDiffWithinAt I I' n f s x \;\land\; f_1 =^{\nhdsWithin s x}_{\text{eventually}} f \land f_1 x = f x \Rightarrow ContMDiffWithinAt I I' n f_1 s x.$$$

Lean4

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

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