contDiffWithinAt_insert_self — Mathlib

English

For any x, ContDiffWithinAt 𝕜 n f (insert x s) x is equivalent to ContDiffWithinAt 𝕜 n f s x.

Русский

Для любой точки x равносильно: ContDiffWithinAt 𝕜 n f (insert x s) x и ContDiffWithinAt 𝕜 n f s x.

LaTeX

$$$\ContDiffWithinAt_{\mathbb{K}}(n,f;\,\mathrm{insert}\;x\;s;x) \quad\Longleftrightarrow\quad \ContDiffWithinAt_{\mathbb{K}}(n,f;\,s;x)$$$

Lean4

theorem contDiffWithinAt_insert_self : ContDiffWithinAt 𝕜 n f (insert x s) x ↔ ContDiffWithinAt 𝕜 n f s x := by
  match n with
  | ω => simp [ContDiffWithinAt]
  | (n : ℕ∞) => simp_rw [ContDiffWithinAt, insert_idem]

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