mul — Mathlib

English

If f and g are C^n on a set s, then their product f·g is C^n on s.

Русский

Если f и g являются C^n на множестве s, то их произведение f·g является C^n на s.

LaTeX

$$$\\\\ContMDiffOn I' I n f s \\\\land \\\\ ContMDiffOn I' I n g s \\\\Rightarrow \\\\ ContMDiffOn I' I n (f \\cdot g) s$$$

Lean4

@[to_additive]
theorem mul (hf : ContMDiffOn I' I n f s) (hg : ContMDiffOn I' I n g s) : ContMDiffOn I' I n (f * g) s := fun x hx =>
  (hf x hx).mul (hg x hx)

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