contDiffAt

Mathlib.Analysis.Calculus.ContDiff.CPolynomial

URI: https://scilib.ai/kg/mathlib#ContinuousMultilinearMap.contDiffAt

English

A continuous multilinear map is smooth in all orders with its coefficient map.

Русский

Мультилінійная карта гладка во всех порядках.

LaTeX

$$$\displaystyle \text{contDiffAt (f : ContinuousMultilinearMap 𝕜 E F) }\; {n} : \ ContDiffAt 𝕜 n (ContinuousMultilinearMap.funLike.coe f)$$$

Lean4

theorem contDiffAt : ContDiffAt 𝕜 n f x :=
  f.cpolynomialAt.contDiffAt

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

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

Разделы

Аффилиация

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