analyticWithinAt_uncurry_of_linear

Mathlib.Analysis.Analytic.CPolynomial

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

← MathLib Explorer

English

Similarly, the uncurried map is analytic on a set s.

Русский

Аналитична функция на множестве s после распаковки.

LaTeX

$$$AnalyticOn_{\mathbb{k}}(p \mapsto f(p_1)(p_2))\, s$$$

Lean4

theorem analyticWithinAt_uncurry_of_linear : AnalyticWithinAt 𝕜 (fun (p : (Π i, Em i) × G) ↦ f p.1 p.2) s x :=
  f.analyticAt_uncurry_of_linear.analyticWithinAt

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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