contDiffAt_apply

Mathlib.Analysis.Calculus.ContDiff.Operations

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

English

The map f ↦ f(i)(j) is ContDiff 𝕜 n.

Русский

Отображение f ↦ f(i)(j) является ContDiff 𝕜 n.

LaTeX

$$$\text{ContDiff } 𝕜 n (\lambda f, f(i)(j))$$$

Lean4

@[fun_prop]
theorem contDiffAt_apply (i : ι) (f : ι → E) : ContDiffAt 𝕜 n (fun f : ι → E => f i) f :=
  (contDiff_apply 𝕜 E i).contDiffAt

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

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

Разделы

Аффилиация

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