mul — Mathlib

English

The product of a finite family of C^n functions is ContDiffWithinAt 𝕜 n on s at x.

Русский

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

LaTeX

$$ContDiffWithinAt 𝕜 n (\prod i ∈ t, f i) s x$$

Lean4

/-- The product of two `C^n` functions at a point is `C^n` at this point. -/
@[fun_prop]
nonrec theorem mul {f g : E → 𝔸} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
    ContDiffAt 𝕜 n (fun x => f x * g x) x :=
  hf.mul hg

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