smul — Mathlib

English

In a vector space, the scalar multiplication map is ContMDiff: the map (f, g) ↦ f · g is ContMDiff when f and g are ContMDiff.

Русский

Векторное пространство: отображение умножения на скаляр гладко зависимо: (f,g) ↦ f·g гладко, если f, g гладкие.

LaTeX

$$$\forall {f: M \to 𝕜} {g: M \to V},\ ContMDiff At I 𝓘(𝕜) n f x \land ContMDiffAt I 𝓘(𝕜, V) n g x \Rightarrow ContMDiffAt I 𝓘(𝕜, V) n (\lambda p: M, f p \cdot g p) x$$$

Lean4

theorem smul {f : M → 𝕜} {g : M → V} (hf : ContMDiffWithinAt I 𝓘(𝕜) n f s x)
    (hg : ContMDiffWithinAt I 𝓘(𝕜, V) n g s x) : ContMDiffWithinAt I 𝓘(𝕜, V) n (fun p => f p • g p) s x :=
  (contMDiff_smul.of_le le_top).contMDiffAt.comp_contMDiffWithinAt x (hf.prodMk hg)

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