contDiffWithinAt_insert — Mathlib

English

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

Русский

Для любого y: ContDiffWithinAt 𝕜 n f (insert y s) x эквивалентно ContDiffWithinAt 𝕜 n f s x.

LaTeX

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

Lean4

theorem contDiffWithinAt_insert {y : E} : ContDiffWithinAt 𝕜 n f (insert y s) x ↔ ContDiffWithinAt 𝕜 n f s x :=
  by
  rcases eq_or_ne x y with (rfl | hx)
  · exact contDiffWithinAt_insert_self
  refine ⟨fun h ↦ h.mono (subset_insert _ _), fun h ↦ ?_⟩
  apply h.mono_of_mem_nhdsWithin
  simp [nhdsWithin_insert_of_ne hx, self_mem_nhdsWithin]

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