contDiffAt_of_subsingleton — Mathlib

English

If F is a subsingleton, then the derivative of f at any point x exists to order n; i.e., f is C^n at x.

Русский

Если F является одиночным, то в любой точке x f удовлетворяет условию C^n; то есть f имеет гладкость C^n в точке x.

LaTeX

$$$ [\text{Subsingleton } F] \Rightarrow \operatorname{ContDiffAt}_{\mathbb{K}}^{n}(f, x) $$$

Lean4

@[nontriviality]
theorem contDiffAt_of_subsingleton [Subsingleton F] : ContDiffAt 𝕜 n f x := by rw [Subsingleton.elim f fun _ => 0];
  exact contDiffAt_const

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