congr_of_eventuallyEq_insert — Mathlib

English

If f1 equals f on the neighborhood of x in insert x s, then ContDiffWithinAt 𝕜 n f1 s x iff ContDiffWithinAt 𝕜 n f s x.

Русский

Если f1 совпадает с f на окрестности x внутри insert x s, то ContDiffWithinAt 𝕜 n f1 s x эквивалентно ContDiffWithinAt 𝕜 n f s x.

LaTeX

$$$ ContDiffWithinAt 𝕜 n f1 s x \\iff ContDiffWithinAt 𝕜 n f s x$$

Lean4

theorem congr_of_eventuallyEq_insert (h : ContDiffWithinAt 𝕜 n f s x) (h₁ : f₁ =ᶠ[𝓝[insert x s] x] f) :
    ContDiffWithinAt 𝕜 n f₁ s x :=
  h.congr_of_eventuallyEq (nhdsWithin_mono x (subset_insert x s) h₁) (mem_of_mem_nhdsWithin (mem_insert x s) h₁ :)

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