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