contDiffWithinAt_prod — Mathlib

English

The product of a family of C^n functions is ContDiffWithinAt 𝕜 n.

Русский

Произведение семейства функций C^n является ContDiffWithinAt 𝕜 n.

LaTeX

$$contDiffWithinAt_prod {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x) : ContDiffWithinAt 𝕜 n (prod i ∈ t, f i) s x$$

Lean4

@[fun_prop]
theorem contDiffWithinAt_prod {t : Finset ι} {f : ι → E → 𝔸'} (h : ∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x) :
    ContDiffWithinAt 𝕜 n (fun y => ∏ i ∈ t, f i y) s x := by
  simpa only [← Finset.prod_apply] using contDiffWithinAt_prod' h

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