congr_contDiffWithinAt_of_mem — Mathlib

English

If nhds x within a set insert x s comply with eq, then ContDiffWithinAt is equivalent after inserting x.

Русский

Если окрестности nhds x внутри множества insert x s совпадают, то ContDiffWithinAt сохраняется после вставки x.

LaTeX

$$$ ContDiffWithinAt 𝕜 n f s x \\to \\forall t, (nhds x).EventuallyEq s t \\Rightarrow ContDiffWithinAt 𝕜 n f t x$$

Lean4

theorem congr_contDiffWithinAt_of_mem (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : x ∈ s) :
    ContDiffWithinAt 𝕜 n f₁ s x ↔ ContDiffWithinAt 𝕜 n f s x :=
  ⟨fun H ↦ H.congr_of_eventuallyEq_of_mem h₁.symm hx, fun H ↦ H.congr_of_eventuallyEq_of_mem h₁ hx⟩

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