analyticOn_uncurry_of_multilinear

English

The uncurry form of a continuous linear map into multilinear maps defines a CPolynomialOn.

Русский

Раскрытая форма непрерывного линейного отображения в мультилейные отображения задаёт CPolynomialOn.

LaTeX

$$cpolynomialOn_uncurry_of_multilinear$$

Lean4

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

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