English
Let Em be a family of normed spaces over a nontrivial normed field 𝕜, G a normed space, and f a continuous multilinear map from the product of the Em i into the space of continuous linear maps G →L𝕜 F. Then the function p ↦ f(p.1) p.2 is a polynomial in the variables p.1 (the first coordinate) with values in F, on the given set s.
Русский
Пусть Em — семейство нормированных пространств над ненулевым нормированным полем 𝕜, G — нормированное пространство, а f — непрерывное много-линейное отображение из произведения Em i в пространство непрерывных линейных отображений G →L𝕜 F. Тогда функция p ↦ f(p.1) p.2 является полиномом по переменным p.1 (первой координате) со значениями в F на заданном множестве s.
LaTeX
$$$CPolynomialOn_{\mathbb{k}}(p \mapsto f(p_1)(p_2))\, s$$$
Lean4
theorem cpolyomialOn_uncurry_of_linear : CPolynomialOn 𝕜 (fun (p : (Π i, Em i) × G) ↦ f p.1 p.2) s := fun _ _ ↦
f.cpolynomialAt_uncurry_of_linear
