curry_left — Mathlib

English

AnalyticOnNhd curry-left: analytic on neighborhoods along the first coordinate.

Русский

AnalyticOnNhd карри-левый: аналитично по первой координате в окрестности.

LaTeX

$$$\\forall f:s\\to t,\\; (AnalyticOnNhd 𝕜 f s) \\Rightarrow AnalyticOnNhd 𝕜 (fun x => f { fst := x, snd := y }) (setOf fun x => x \\in s) $$

Lean4

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

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