contMDiffAt_finset_prod — Mathlib

English

Let t be a finite set and f_i : M → G. If each f_i is ContMDiffAt at x, then the map x ↦ ∏_{i∈t} f_i(x) is ContMDiffAt at x.

Русский

Пусть t — конечное множество, f_i : M → G. Если каждый f_i является ContMDiffAt в x, то отображение x ↦ ∏_{i∈t} f_i(x) является ContMDiffAt в x.

LaTeX

$$$( \forall i \in t, \ ContMDiffAt I' I n (f i) x ) \to \ ContMDiffAt I' I n (\lambda x, \prod_{i \in t} f_i(x)) x$$$

Lean4

@[to_additive]
theorem contMDiffAt_finset_prod (h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x) :
    ContMDiffAt I' I n (fun x => ∏ i ∈ t, f i x) x :=
  contMDiffWithinAt_finset_prod h

Похожие утверждения