inner — Mathlib

English

For 𝕜, E, F with RCLike 𝕜 and inner product spaces, ContDiff Real n f, ContDiff Real n g implies ContDiff Real n (λx, ⟪f x, g x⟫).

Русский

При наличии 𝕜-внутреннего произведения и параметров, если f,g ContDiff Real n, то их скалярное произведение inner также ContDiff Real n.

LaTeX

$$$\\operatorname{ContDiff}_{\\mathbb{R}} n\\ f\\ g \\Rightarrow \\operatorname{ContDiff}_{\\mathbb{R}} n\\ (x \\mapsto \\langle f(x), g(x)\\rangle).$$$

Lean4

theorem inner (hf : ContDiff ℝ n f) (hg : ContDiff ℝ n g) : ContDiff ℝ n fun x => ⟪f x, g x⟫ :=
  contDiff_inner.comp (hf.prodMk hg)

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