English
If a finite family f_i is ContMDiffWithinAt on s near x0, then the finite product is ContMDiffWithinAt on s near x0.
Русский
Если конечная семья функций f_i непрерывно-дифференцируема на s вблизи x0, то их конечное произведение тоже непрерывно-дифференцируемо на s вблизи x0.
LaTeX
$$$\\\\forall i \\\\in t, \\\\ ContMDiffWithinAt I' I n (f_i) s x_0 \\\\Rightarrow \\\\ ContMDiffWithinAt I' I n (\\\\lambda x, \\\\prod_{i \\\\in t} f_i(x)) s x_0$$$
Lean4
@[to_additive]
theorem prod (h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x₀) :
ContMDiffWithinAt I' I n (fun x ↦ ∏ i ∈ t, f i x) s x₀ := by
classical
induction t using Finset.induction_on with
| empty => simp [contMDiffWithinAt_const]
| insert i K iK IH =>
simp only [iK, Finset.prod_insert, not_false_iff]
exact (h _ (Finset.mem_insert_self i K)).mul (IH fun j hj ↦ h _ <| Finset.mem_insert_of_mem hj)
