curry_right — Mathlib

English

The curry-right principle: analytic functions on products are analytic in the second coordinate.

Русский

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

LaTeX

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

Lean4

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

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