curry_left — Mathlib

English

If fa is ContMDiffWithinAt for uncurry f, then the map y ↦ f x y is ContMDiffWithinAt.

Русский

Если fa — C^n для uncurry f, то отображение y ↦ f x y гладкое в пределах.

LaTeX

$$$\\displaystyle \\operatorname{ContMDiffWithinAt} \\; I' \\; J \\; n \\; (f \\; x) \\; y \\; \\text{is ContMDiffWithinAt}$$$

Lean4

/-- Curried `C^n` functions are `C^n` in the first coordinate. -/
theorem curry_left {f : M → M' → N} {x : M} {y : M'} {s : Set (M × M')}
    (fa : ContMDiffWithinAt (I.prod I') J n (uncurry f) s (x, y)) :
    ContMDiffWithinAt I J n (fun x ↦ f x y) {x | (x, y) ∈ s} x :=
  fa.comp₂ contMDiffWithinAt_id contMDiffWithinAt_const (fun _ h ↦ h)

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