English
Let E, F, G be normed spaces over a nontrivially normed field 𝕜, and let f be a continuous bilinear map E × F → G. Then the map (x, y) ↦ f(x, y) is analytic on the product space E × F; in particular it is analytic at every point and analytic on every subset s ⊆ E × F.
Русский
Пусть E, F, G — нормированные пространства над ненулевым полем 𝕜, и пусть f — непрерывное билинейное отображение E × F → G. Тогда отображение (x, y) ↦ f(x, y) аналитично на произведении пространств E × F; в частности, аналитично в каждой точке и на любом подмножестве s ⊆ E × F.
LaTeX
$$$AnalyticWithinAt 𝕜 (\\lambda p : E \\times F. f(p.1, p.2)) s x$$$
Lean4
protected theorem analyticWithinAt_bilinear (f : E →L[𝕜] F →L[𝕜] G) (s : Set (E × F)) (x : E × F) :
AnalyticWithinAt 𝕜 (fun x : E × F => f x.1 x.2) s x :=
(f.analyticAt_bilinear x).analyticWithinAt
