mul — Mathlib

English

The product of two C^n functions is C^n.

Русский

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

LaTeX

$$ContDiff 𝕜 n (\lambda p => p.1 * p.2) = ContDiff 𝕜 n fun p => p.1 * p.2$$

Lean4

/-- The product of two `C^n` functions on a domain is `C^n`. -/
@[fun_prop]
theorem mul {f g : E → 𝔸} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) : ContDiffOn 𝕜 n (fun x => f x * g x) s :=
  fun x hx => (hf x hx).mul (hg x hx)

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