curry_left — Mathlib

English

AnalyticWithinAt curry-left: analytic within a sliced domain along the first coordinate.

Русский

Карри-левый внутри: аналитичность внутри области по первой координате.

LaTeX

$$$\\forall f:\\u03a5\\times\\u03a6 \\to \\u0397,\\; s\\subseteq E\\times F,\\; p=(x,y)\\in s,\\ (AnalyticWithinAt 𝕜 f s p) \\Rightarrow AnalyticWithinAt 𝕜 (fun x \\mapsto f (x, p.2)) {x| (x,p.2)\\in s} p.1$$$

Lean4

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

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