mul — Mathlib

English

If f and g are ContMDiff on the whole space, then their product f·g is ContMDiff on the space.

Русский

Если f и g являются ContMDiff на всей области, то их произведение f·g также ContMDiff на этой области.

LaTeX

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

Lean4

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

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