curry_right — Mathlib

English

Analytic functions on products are analytic in the second coordinate.

Русский

Аналитические функции на произведении аналитичны во второй координате.

LaTeX

$$$\\forall f:\\u03a6\\times\\u03a0 \\to \\u0393,\\; p=(x,y)\\in E\\times F,\\; (AnalyticAt 𝕜 f p) \\Rightarrow AnalyticAt 𝕜 (fun y \\mapsto f (p.1, y)) p.2$$$

Lean4

theorem curry_right {f : E × F → G} {s : Set (E × F)} {p : E × F} (fa : AnalyticWithinAt 𝕜 f s p) :
    AnalyticWithinAt 𝕜 (fun y ↦ f (p.1, y)) {y | (p.1, y) ∈ s} p.2 :=
  AnalyticWithinAt.comp₂ fa analyticWithinAt_const analyticWithinAt_id (fun _ hx ↦ hx)

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