contDiffWithinAt_fun_id

Mathlib.Analysis.Calculus.ContDiff.Basic

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

English

For any set s, the identity map id: E → E is ContDiffOn 𝕜 n on s.

Русский

Для любого множества s тождественное отображение id: E → E гладко на s: ContDiffOn 𝕜 n id s.

LaTeX

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

Lean4

@[fun_prop]
theorem contDiffWithinAt_fun_id {s x} : ContDiffWithinAt 𝕜 n (fun x : E => x) s x :=
  contDiff_id.contDiffWithinAt

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

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

Разделы

Аффилиация

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