curry_left — Mathlib

English

The product map is ContMDiff if both individual maps are ContMDiff

Русский

Произведение карт гладко, если обе карты гладкие

LaTeX

$$$\\displaystyle \\operatorname{ContMDiff} \\; \\text{(prodMap')} \\; f \\; g = \\text{ ContMDiff }$$

Lean4

/-- Curried `C^n` functions are `C^n` in the first coordinate. -/
theorem curry_left {f : M → M' → N} (fa : ContMDiff (I.prod I') J n (uncurry f)) {y : M'} :
    ContMDiff I J n (fun x ↦ f x y) := fun _ ↦ (fa _).along_fst

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