contDiffAt_id

Mathlib.Analysis.Calculus.ContDiff.Basic

URI: https://scilib.ai/kg/mathlib#contDiffAt_id

English

The function f ↦ x is C^n within set s at x, i.e., the identity function on the domain is C^n when composed with f.

Русский

Функция f(x) = x находится в C^n внутри множества s в точке x.

LaTeX

$$$ \operatorname{ContDiffWithinAt}_{\mathbb{K}}^{n}(\mathrm{id}, s, x) $$$

Lean4

theorem contDiffAt_id {x} : ContDiffAt 𝕜 n (id : E → E) x :=
  contDiff_id.contDiffAt

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru