insert — Mathlib

English

If h is ContDiffWithinAt 𝕜 n f s x in ContDiffWithinAt namespace, then inserting x into s preserves ContDiffWithinAt at x.

Русский

Если h = ContDiffWithinAt 𝕜 n f s x, то вставка x в s сохраняет ContDiffWithinAt в точке x.

LaTeX

$$$\text{ContDiffWithinAt}_{\mathbb{K}}(n,f;s\cup\{x\},x) \\ Longrightarrow \\ ContDiffWithinAt_{\mathbb{K}}(n,f;\mathrm{insert}\;x\;s,x)$$$

Lean4

protected theorem insert (h : ContDiffWithinAt 𝕜 n f s x) : ContDiffWithinAt 𝕜 n f (insert x s) x :=
  h.insert'

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