contDiff_prodMk_right — Mathlib

English

If hf and hg are ContDiffWithinAt 𝕜 n for f on s at x and g on t at y, then Prod.map f g is ContDiffWithinAt 𝕜 n on (s×ˢ t) at (x,y).

Русский

Если hf и hg — ContDiffWithinAt 𝕜 n для f на s в x и для g на t в y, то Prod.map f g — ContDiffWithinAt 𝕜 n на s×t в (x,y).

LaTeX

$$$\\forall \\{f\\,g\\,s\\,t\\,x\\,y\\},\\; \\mathrm{ContDiffWithinAt}_{\\mathbb{k}}\\ n\\ f\\ s\\ x \\to \\mathrm{ContDiffWithinAt}_{\\mathbb{k}}\\ n\\ g\\ t\\ y \\to \\mathrm{ContDiffWithinAt}_{\\mathbb{k}}\\ n\\ (\\mathrm{Prod.map}\\ f\\ g)\\ (s\\timesˢ t)\\ (x,y)$$$

Lean4

@[fun_prop]
theorem contDiff_prodMk_right (e₀ : E) : ContDiff 𝕜 n fun f : F => (e₀, f) :=
  contDiff_const.prodMk contDiff_id

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