English
Let t be a Finset ι and f_i: E → F be ContDiff 𝕜 n at x for all i ∈ t. Then the map y ↦ ∏_{i∈t} f_i(y) is ContDiff 𝕜 n at x.
Русский
Пусть t — конечное множество индексов, и для каждого i ∈ t функция f_i: E → F принадлежит к классу ContDiff 𝕜 n в x. Тогда отображение y ↦ ∏_{i∈t} f_i(y) гладкое до порядка n в x.
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 contDiffAt_prod {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffAt 𝕜 n (f i) x) :
ContDiffAt 𝕜 n (fun y => ∏ i ∈ t, f i y) x :=
contDiffWithinAt_prod h
