contDiffWithinAt_of_subsingleton — Mathlib

English

If F is a subsingleton, then f is C^n within any set s at any point x in s.

Русский

Если F единичен, то f обладает гладкостью C^n внутри произвольного множества s в точке x, принадлежащей s.

LaTeX

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

Lean4

@[nontriviality]
theorem contDiffWithinAt_of_subsingleton [Subsingleton F] : ContDiffWithinAt 𝕜 n f s x := by
  rw [Subsingleton.elim f fun _ => 0]; exact contDiffWithinAt_const

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