analyticAt_uncurry_of_linear

Mathlib.Analysis.Analytic.CPolynomial

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

English

For the same setting, the uncurried map is analytic at a point x.

Русский

Для той же установки распакованная карта аналитична в точке x.

LaTeX

$$$AnalyticAt_{\mathbb{k}}(p \mapsto f(p_1)(p_2))\, x$$$

Lean4

theorem analyticAt_uncurry_of_linear : AnalyticAt 𝕜 (fun (p : (Π i, Em i) × G) ↦ f p.1 p.2) x :=
  f.cpolynomialAt_uncurry_of_linear.analyticAt

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

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

Разделы

Аффилиация

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