congr_contDiffWithinAt — Mathlib

English

If f and f1 are eventually equal along nhdsWithin, then ContDiffWithinAt for f implies the same for f1, and the equality of values at x matches.

Русский

Если f и f1 равны почти всюду в окрестности nhdsWithin, то ContDiffWithinAt для f переходят к f1, и значения в x совпадают.

LaTeX

$$$ ContDiffWithinAt 𝕜 n f s x \\land (f1 =^\\!\\[𝓝[s] x\\] f) \\land (f1 x = f x) \\Rightarrow ContDiffWithinAt 𝕜 n f1 s x$$

Lean4

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

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