analyticOnNhd_bilinear — Mathlib

English

Let E, F, G be normed spaces over 𝕜 and f: E × F → G a bilinear map as above. Then the function (x, y) ↦ f(x, y) is analytic on some neighborhood of every point; more precisely, it is AnalyticOnNhd 𝕜 (x, y) ↦ f(x, y) on any subset s ⊆ E × F.

Русский

Пусть E, F, G — нормированные пространства над 𝕜 и f: E × F → G билinear; тогда отображение (x, y) ↦ f(x, y) аналитично на окрестности любых точек, т. е. AnalyticOnNhd 𝕜 (x, y) ↦ f(x, y) на произвольном s ⊆ E × F.

LaTeX

$$$AnalyticOnNhd 𝕜 (\\lambda p : E \\times F. f(p.1, p.2)) s$$$

Lean4

protected theorem analyticOnNhd_bilinear (f : E →L[𝕜] F →L[𝕜] G) (s : Set (E × F)) :
    AnalyticOnNhd 𝕜 (fun x : E × F => f x.1 x.2) s := fun x _ ↦ f.analyticAt_bilinear x

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