analyticOn_uncurry_of_linear

Mathlib.Analysis.Analytic.CPolynomial

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

English

The uncurried map p ↦ f(p.1) p.2 is analytic on the underlying set s.

Русский

Распакованная карта p ↦ f(p.1) p.2 аналитична на множестве s.

LaTeX

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

Lean4

theorem analyticOn_uncurry_of_linear : AnalyticOn 𝕜 (fun (p : (Π i, Em i) × G) ↦ f p.1 p.2) s :=
  f.analyticOnNhd_uncurry_of_linear.analyticOn

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

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

Разделы

Аффилиация

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