contDiffWithinAt_singleton — Mathlib

English

For a singleton set {x}, f is C^n at x within that singleton: ContDiffWithinAt 𝕜 n f {x} x.

Русский

Для множества-синглтона {x} функция f гладка в точке x внутри этого множества: ContDiffWithinAt 𝕜 n f {x} x.

LaTeX

$$$ \operatorname{ContDiffWithinAt}_{\mathbb{K}}^{n}(f, \{x\}, x) $$$

Lean4

theorem contDiffWithinAt_singleton : ContDiffWithinAt 𝕜 n f { x } x :=
  (contDiffWithinAt_const (c := f x)).congr (by simp) rfl

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