contMDiffAt_finset_prod' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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