English
Let t be Finset ι and f: ι → E → 𝔸' be ContDiff 𝕜 n. Then the product ∏_{i∈t} f_i is ContDiff 𝕜 n.
Русский
Пусть t — конечное множество индексов, и f_i: E → 𝔸' гладкие до порядка n. Тогда произведение по i∈t гладко до порядка n.
LaTeX
$$$\\\\forall t \\\\in \\\\mathrm{Finset} \\\\; ι \\\\; \\\\forall f : ι \\\\to E \\\\to \\\\mathbb{A}', \\\\left( \\\\forall i \\\\in t, \ ContDiff 𝕜 n \\\\left( f i \right) \right) \\\\\\Rightarrow \ ContDiff 𝕜 n \\\\left( \\lambda y, \\\\prod_{i \\\\in t} f i(y) \\\\right)$$
Lean4
@[fun_prop]
theorem contDiff_prod {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiff 𝕜 n (f i)) :
ContDiff 𝕜 n fun y => ∏ i ∈ t, f i y :=
contDiff_iff_contDiffAt.mpr fun _ => contDiffAt_prod fun i hi => (h i hi).contDiffAt
