smul — Mathlib

English

On a charted space, the smul operation is smooth for ContMDiffOn: if f,g are ContMDiffOn, then x ↦ f(x)·g(x) is ContMDiffOn.

Русский

На гладком пространстве – операция умножения на скаляр гладкая в контексте ContMDiffOn.

LaTeX

$$$\forall {f : M \to 𝕜} {g : M \to V},\ ContMDiffOn I 𝓘(𝕜) n f s \rightarrow ContMDiffOn I 𝓘(𝕜, V) n g s \rightarrow ContMDiffOn I 𝓘(𝕜, V) n (fun p => f p \cdot g p) s$$$

Lean4

theorem smul {f : M → 𝕜} {g : M → V} (hf : ContMDiffOn I 𝓘(𝕜) n f s) (hg : ContMDiffOn I 𝓘(𝕜, V) n g s) :
    ContMDiffOn I 𝓘(𝕜, V) n (fun p => f p • g p) s := fun x hx => (hf x hx).smul (hg x hx)

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