mul — Mathlib

English

The product of two C^n functions on a domain is C^n on that domain.

Русский

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

LaTeX

$$ContDiffWithinAt 𝕜 n f s x ∧ ContDiffWithinAt 𝕜 n g s x ⇒ ContDiffWithinAt 𝕜 n (fun x => f x * g x) s x$$

Lean4

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

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