curry_right — Mathlib

English

AnalyticOnNhd curry-right: analytic on neighborhoods in the second coordinate.

Русский

AnalyticOnNhd curry-right: аналитично во второй координате рядом с точкой.

LaTeX

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

Lean4

/-- Analytic functions on products are analytic in the second coordinate -/
theorem curry_right {f : E × F → G} {x : E} {s : Set (E × F)} (fa : AnalyticOnNhd 𝕜 f s) :
    AnalyticOnNhd 𝕜 (fun y ↦ f (x, y)) {y | (x, y) ∈ s} := fun y m ↦ (fa (x, y) m).curry_right

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