contDiffWithinAt_diff_singleton — Mathlib

English

Removing a point y from s does not affect C^n within at x: ContDiffWithinAt 𝕜 n f (s \ {y}) x ↔ ContDiffWithinAt 𝕜 n f s x.

Русский

Удаление точки y из области s не изменяет ContDiffWithinAt в x.

LaTeX

$$$\ContDiffWithinAt_{\mathbb{K}}(n,f;\,s\setminus\{y\},x) \iff \ContDiffWithinAt_{\mathbb{K}}(n,f;\,s,x)$$$

Lean4

theorem contDiffWithinAt_diff_singleton {y : E} : ContDiffWithinAt 𝕜 n f (s \ { y }) x ↔ ContDiffWithinAt 𝕜 n f s x :=
  by rw [← contDiffWithinAt_insert, insert_diff_singleton, contDiffWithinAt_insert]

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