insert — Mathlib

English

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

Русский

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

LaTeX

$$$$MDifferentiableWithinAt I I' f s x \\rightarrow MDifferentiableWithinAt I I' f (insert x s) x$$$$

Lean4

protected theorem insert (h : MDifferentiableWithinAt I I' f s x) : MDifferentiableWithinAt I I' f (insert x s) x :=
  h.insert'

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