contDiffWithinAt_prod' — Mathlib

English

The product of finitely many 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 (∏ 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 (∏ i ∈ t, f i) s x :=
  Finset.prod_induction f (fun f => ContDiffWithinAt 𝕜 n f s x) (fun _ _ => ContDiffWithinAt.mul)
    (contDiffWithinAt_const (c := 1)) h

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