insert — Mathlib

English

If f is differentiable within s at x, then f is differentiable within insert x s at x.

Русский

Если f дифференцируема внутри s в x, то она дифференцируема внутри insert x s в x.

LaTeX

$$$\text{DifferentiableWithinAt } 𝕜 f s x \Rightarrow \text{DifferentiableWithinAt } 𝕜 f (\mathrm{Set.insert} x\, s) x$$$

Lean4

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

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