English
If f and f1 agree on s and x ∈ s, then ContDiffWithinAt is preserved from f to f1.
Русский
Если f и f1 совпадают на s и x принадлежит s, ContDiffWithinAt сохраняется при переходе от f к f1.
LaTeX
$$$ ContDiffWithinAt 𝕜 n f s x \\Rightarrow (∀ y∈s, f1 y = f y) \\Rightarrow x ∈ s \\Rightarrow ContDiffWithinAt 𝕜 n f1 s x$$
Lean4
theorem contDiffWithinAt_congr (h₁ : ∀ y ∈ s, f₁ y = f y) (hx : f₁ x = f x) :
ContDiffWithinAt 𝕜 n f₁ s x ↔ ContDiffWithinAt 𝕜 n f s x :=
⟨fun h' ↦ h'.congr (fun x hx ↦ (h₁ x hx).symm) hx.symm, fun h' ↦ h'.congr h₁ hx⟩