contDiffWithinAt — Mathlib

English

The containment of differentiability for bumps holds for all s; i.e., ContDiffWithinAt Real (WithTop.some n) f s x is true for all s.

Русский

Утверждение о дифференцируемости бамп-функции внутри любых множеств.

LaTeX

$$$\\forall {s:Set E}, ContDiffWithinAt Real (WithTop.some n) f s x$$

Lean4

protected theorem contDiffWithinAt {s : Set E} : ContDiffWithinAt ℝ n f s x :=
  f.contDiffAt.contDiffWithinAt

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