contDiff_prodMk_left — Mathlib

English

The product map of two C^n functions within a set is C^n on the product set, with p as pair.

Русский

Произведение двух функций класса C^n внутри указанных множеств является C^n на произведении множеств.

LaTeX

$$$\\mathrm{ContDiffWithinAt}_{\\mathbb{k}}\\ n\\ f\\ s\\ p.1 \\to \\mathrm{ContDiffWithinAt}_{\\mathbb{k}}\\ n\\ g\\ t\\ p.2 \\to \\mathrm{ContDiffWithinAt}_{\\mathbb{k}}\\ n\\ \\mathrm{Prod.map}\\ f\\ g\\ (s×ˢ t)\\ p$$$

Lean4

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

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