English
Let t be a finite set of indices ι and for each i in t let f_i: E → 𝔸' be differentiable to C^n at x. If every f_i is ContDiffAt 𝕜 n at x, then the product function y ↦ ∏_{i∈t} f_i(y) is ContDiffAt 𝕜 n at x.
Русский
Пусть t — конечное множество индексов ι, и для каждого i в t функции f_i: E → 𝔸' достаточно гладкие в точке x. Если для каждого i ∈ t выполняется ContDiffAt 𝕜 n (f_i) в 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, \ ContDiffAt \\\\mathbb{K} n \\\\left( f_i \right) x \right) \\\\Rightarrow \ ContDiffAt \\\\mathbb{K} 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 (∏ i ∈ t, f i) x :=
contDiffWithinAt_prod' h
