analyticOn_bilinear — Mathlib

English

Let E, F, G be normed spaces over 𝕜 and f: E →L[𝕜] F →L[𝕜] G a bilinear map. Then the map (x, y) ↦ f(x, y) is analytic on any subset s ⊆ E × F; i.e., AnalyticOn 𝕜 (x, y) ↦ f(x, y) on s.

Русский

Пусть E, F, G — нормированные пространства над 𝕜 и f: E →L[𝕜] F →L[𝕜] G — билинейное отображение. Тогда (x, y) ↦ f(x, y) аналитично на любом подмножестве s ⊆ E × F; то есть AnalyticOn 𝕜 (x, y) ↦ f(x, y) на s.

LaTeX

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

Lean4

protected theorem analyticOn_bilinear (f : E →L[𝕜] F →L[𝕜] G) (s : Set (E × F)) :
    AnalyticOn 𝕜 (fun x : E × F => f x.1 x.2) s :=
  (f.analyticOnNhd_bilinear s).analyticOn

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