contDiff_mul — 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 ∧ ContDiffWithinAt 𝕜 n g s x ⇒ ContDiffWithinAt 𝕜 n (fun x => f x * g x) s x$$

Lean4

@[fun_prop]
theorem contDiff_mul : ContDiff 𝕜 n fun p : 𝔸 × 𝔸 => p.1 * p.2 :=
  (ContinuousLinearMap.mul 𝕜 𝔸).isBoundedBilinearMap.contDiff

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