curry_left — Mathlib

English

Analytic functions on products are analytic in the first coordinate.

Русский

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

LaTeX

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

Lean4

/-- Analytic functions on products are analytic in the first coordinate -/
theorem curry_left {f : E × F → G} {p : E × F} (fa : AnalyticAt 𝕜 f p) : AnalyticAt 𝕜 (fun x ↦ f (x, p.2)) p.1 :=
  AnalyticAt.comp₂ fa analyticAt_id analyticAt_const

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