sum — Mathlib

English

The product of two C^n functions within a set is C^n at that point.

Русский

Произведение двух функций C^n на заданной области внутри точки является C^n.

LaTeX

$$ContDiffWithinAt 𝕜 n f s x \land ContDiffWithinAt 𝕜 n g s x → ContDiffWithinAt 𝕜 n (\lambda y. f y * g y) s x$$

Lean4

@[fun_prop]
theorem sum {ι : Type*} {f : ι → E → F} {s : Finset ι} {t : Set E} (h : ∀ i ∈ s, ContDiffOn 𝕜 n (fun x => f i x) t) :
    ContDiffOn 𝕜 n (fun x => ∑ i ∈ s, f i x) t := fun x hx => ContDiffWithinAt.sum fun i hi => h i hi x hx

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