curry_left — Mathlib

English

AnalyticOn curry-left for functions on product spaces: the curry-left map is analytic.

Русский

Аналитика карри-левого отображения на произведении пространств.

LaTeX

$$$\\forall f:\\u03a5\\times\\u03a6 \\to \\u0397,\\; (AnalyticOn 𝕜 f s) \\Rightarrow AnalyticOn 𝕜 (fun x => f { fst := x, snd := y }) (setOf fun x => x \\in s)$$$

Lean4

theorem curry_left {f : E × F → G} {s : Set (E × F)} {y : F} (fa : AnalyticOn 𝕜 f s) :
    AnalyticOn 𝕜 (fun x ↦ f (x, y)) {x | (x, y) ∈ s} := fun x m ↦ (fa (x, y) m).curry_left

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