analyticOnNhd_uncurry_of_linear — Mathlib

English

The uncurried function p ↦ f(p.1) p.2 is analytic on nhds of every point in s, given f as above.

Русский

Функция без куррирования p ↦ f(p.1) p.2 аналитична в окрестности любой точки множества s.

LaTeX

$$$AnalyticOnNhd_{\\mathbb{k}}(p \\mapsto f(p_1)(p_2))\\, s$$$

Lean4

theorem analyticOnNhd_uncurry_of_linear : AnalyticOnNhd 𝕜 (fun (p : (Π i, Em i) × G) ↦ f p.1 p.2) s :=
  f.cpolyomialOn_uncurry_of_linear.analyticOnNhd

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